This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1397

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1397.1 ⊢ φ → ∃ x ψ
bnj1397.2 ⊢ ψ → ∀ x ψ
Assertion bnj1397 ⊢ φ → ψ

Proof

Step Hyp Ref Expression
1 bnj1397.1 ⊢ φ → ∃ x ψ
2 bnj1397.2 ⊢ ψ → ∀ x ψ
3 2 19.9h ⊢ ∃ x ψ ↔ ψ
4 1 3 sylib ⊢ φ → ψ