http://us2.metamath.org:8888/mpeuni/mmrecent.html Recent proofs for Metamath proof system en http://feedproxy.google.com/~r/MetamathRecentProofs/~3/19EyHXIDuHs/lanfwcl.html 15-Jul-2009   ⊢ X = dom R    ⇒
   ⊢ ((R ∈ Lat ⋀ A ∈ X ⋀ B ∈ X) → (R inf_w {A, B}) ∈ X)
    ]]> http://us2.metamath.org:8888/mpeuni/lanfwcl.html http://feedproxy.google.com/~r/MetamathRecentProofs/~3/kdKtazsUu0g/conntoppr.html 8-Jul-2009   ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ J ~= K) → (J ∈ Con ↔ K ∈ Con))
    ]]> http://us2.metamath.org:8888/mpeuni/conntoppr.html http://feedproxy.google.com/~r/MetamathRecentProofs/~3/YnOdvbOYmps/conntopprlem.html 8-Jul-2009conntoppr 11095.
   ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ J ~= K) → (J ∈ Con → K ∈ Con))
    ]]> http://us2.metamath.org:8888/mpeuni/conntopprlem.html http://feedproxy.google.com/~r/MetamathRecentProofs/~3/yXRlCQhFykQ/hmeocldb.html 8-Jul-2009   ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ (J Homeo K)) ⋀ S ∈ (Clsd ‘K)) → (^◡F “ S) ∈ (Clsd ‘J))
    ]]> http://us2.metamath.org:8888/mpeuni/hmeocldb.html http://feedproxy.google.com/~r/MetamathRecentProofs/~3/ei9714sd6us/hmeoclda.html 8-Jul-2009   ⊢ (((J ∈ Top ⋀ K ∈ Top ⋀ F ∈ (J Homeo K)) ⋀ S ∈ (Clsd ‘J)) → (F “ S) ∈ (Clsd ‘K))
    ]]> http://us2.metamath.org:8888/mpeuni/hmeoclda.html http://feedproxy.google.com/~r/MetamathRecentProofs/~3/yPq5f_q_H-k/dn1.html 8-Jul-20091. See http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf. (Contributed by Jeffrey Hankins, 3-Jul-2009.)
   ⊢ (¬ (¬ (¬ (φ ⋁ ψ) ⋁ χ) ⋁ ¬ (φ ⋁ ¬ (¬ χ ⋁ ¬ (χ ⋁ θ)))) ↔ χ)
    ]]> http://us2.metamath.org:8888/mpeuni/dn1.html http://feedproxy.google.com/~r/MetamathRecentProofs/~3/X5u4uq-Tfsc/comptoppr.html 3-Jul-2009   ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ J ~= K) → (J ∈ Comp ↔ K ∈ Comp))
    ]]> http://us2.metamath.org:8888/mpeuni/comptoppr.html http://feedproxy.google.com/~r/MetamathRecentProofs/~3/7SUJJwmfeO8/comptopprlem.html 3-Jul-2009comptoppr 11091.
   ⊢ ((J ∈ Top ⋀ K ∈ Top ⋀ J ~= K) → (J ∈ Comp → K ∈ Comp))
    ]]> http://us2.metamath.org:8888/mpeuni/comptopprlem.html http://feedproxy.google.com/~r/MetamathRecentProofs/~3/XGRN-a4VR_4/com15.html 3-Jul-2009   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒
   ⊢ (τ → (ψ → (χ → (θ → (φ → η)))))
    ]]> http://us2.metamath.org:8888/mpeuni/com15.html http://feedproxy.google.com/~r/MetamathRecentProofs/~3/QZvWYzO6jxI/com45.html 3-Jul-2009   ⊢ (φ → (ψ → (χ → (θ → (τ → η)))))    ⇒
   ⊢ (φ → (ψ → (χ → (τ → (θ → η)))))]]> http://us2.metamath.org:8888/mpeuni/com45.html