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

Metamath Proof Explorer

Theorem bnj596

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

Ref Expression
Hypotheses bnj596.1 ⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
bnj596.2 ⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
Assertion bnj596 ( 𝜑 → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 bnj596.1 ⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2 bnj596.2 ⊢ ( 𝜑 → ∃ 𝑥 𝜓 )
3 2 ancli ⊢ ( 𝜑 → ( 𝜑 ∧ ∃ 𝑥 𝜓 ) )
4 1 nf5i ⊢ Ⅎ 𝑥 𝜑
5 4 19.42 ⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃ 𝑥 𝜓 ) )
6 3 5 sylibr ⊢ ( 𝜑 → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )