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 ⊢ ∃ x φ ∨ ψ ↔ ∃ x φ ∨ ∃ x ψ

Proof

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