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 ( 𝜑 → ∃ 𝑥 ( 𝜑𝜓 ) )