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

Metamath Proof Explorer

Theorem 19.43OLD

Description: Obsolete proof of 19.43 . Do not delete as it is referenced on the mmrecent.html page and in conventions-labels . (Contributed by NM, 5-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 19.43OLD ( ∃ 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∨ ∃ 𝑥 𝜓 ) )

Proof

Step Hyp Ref Expression
1 ioran ⊢ ( ¬ ( 𝜑 ∨ 𝜓 ) ↔ ( ¬ 𝜑 ∧ ¬ 𝜓 ) )
2 1 albii ⊢ ( ∀ 𝑥 ¬ ( 𝜑 ∨ 𝜓 ) ↔ ∀ 𝑥 ( ¬ 𝜑 ∧ ¬ 𝜓 ) )
3 19.26 ⊢ ( ∀ 𝑥 ( ¬ 𝜑 ∧ ¬ 𝜓 ) ↔ ( ∀ 𝑥 ¬ 𝜑 ∧ ∀ 𝑥 ¬ 𝜓 ) )
4 alnex ⊢ ( ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∃ 𝑥 𝜑 )
5 alnex ⊢ ( ∀ 𝑥 ¬ 𝜓 ↔ ¬ ∃ 𝑥 𝜓 )
6 4 5 anbi12i ⊢ ( ( ∀ 𝑥 ¬ 𝜑 ∧ ∀ 𝑥 ¬ 𝜓 ) ↔ ( ¬ ∃ 𝑥 𝜑 ∧ ¬ ∃ 𝑥 𝜓 ) )
7 2 3 6 3bitri ⊢ ( ∀ 𝑥 ¬ ( 𝜑 ∨ 𝜓 ) ↔ ( ¬ ∃ 𝑥 𝜑 ∧ ¬ ∃ 𝑥 𝜓 ) )
8 7 notbii ⊢ ( ¬ ∀ 𝑥 ¬ ( 𝜑 ∨ 𝜓 ) ↔ ¬ ( ¬ ∃ 𝑥 𝜑 ∧ ¬ ∃ 𝑥 𝜓 ) )
9 df-ex ⊢ ( ∃ 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ¬ ∀ 𝑥 ¬ ( 𝜑 ∨ 𝜓 ) )
10 oran ⊢ ( ( ∃ 𝑥 𝜑 ∨ ∃ 𝑥 𝜓 ) ↔ ¬ ( ¬ ∃ 𝑥 𝜑 ∧ ¬ ∃ 𝑥 𝜓 ) )
11 8 9 10 3bitr4i ⊢ ( ∃ 𝑥 ( 𝜑 ∨ 𝜓 ) ↔ ( ∃ 𝑥 𝜑 ∨ ∃ 𝑥 𝜓 ) )