Theorem 19.43OLD 1606

Description: Obsolete proof of 19.43 1605 as of 3-May-2016. Leave this in for the example on the mmrecent.html page. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
19.43OLD	⊢ (∃x(φ ∨ ψ) ↔ (∃xφ ∨ ∃xψ))

Proof of Theorem 19.43OLD

Step	Hyp	Ref	Expression
1		ioran 476	. . . . 5 ⊢ (¬ (φ ∨ ψ) ↔ (¬ φ ∧ ¬ ψ))
2	1	albii 1566	. . . 4 ⊢ (∀x ¬ (φ ∨ ψ) ↔ ∀x(¬ φ ∧ ¬ ψ))
3		19.26 1593	. . . 4 ⊢ (∀x(¬ φ ∧ ¬ ψ) ↔ (∀x ¬ φ ∧ ∀x ¬ ψ))
4		alnex 1543	. . . . 5 ⊢ (∀x ¬ φ ↔ ¬ ∃xφ)
5		alnex 1543	. . . . 5 ⊢ (∀x ¬ ψ ↔ ¬ ∃xψ)
6	4, 5	anbi12i 678	. . . 4 ⊢ ((∀x ¬ φ ∧ ∀x ¬ ψ) ↔ (¬ ∃xφ ∧ ¬ ∃xψ))
7	2, 3, 6	3bitri 262	. . 3 ⊢ (∀x ¬ (φ ∨ ψ) ↔ (¬ ∃xφ ∧ ¬ ∃xψ))
8	7	notbii 287	. 2 ⊢ (¬ ∀x ¬ (φ ∨ ψ) ↔ ¬ (¬ ∃xφ ∧ ¬ ∃xψ))
9		df-ex 1542	. 2 ⊢ (∃x(φ ∨ ψ) ↔ ¬ ∀x ¬ (φ ∨ ψ))
10		oran 482	. 2 ⊢ ((∃xφ ∨ ∃xψ) ↔ ¬ (¬ ∃xφ ∧ ¬ ∃xψ))
11	8, 9, 10	3bitr4i 268	1 ⊢ (∃x(φ ∨ ψ) ↔ (∃xφ ∨ ∃xψ))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 176   ∨ wo 357   ∧ wa 358  ∀wal 1540  ∃wex 1541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This proof depends on definitions:  df-bi 177  df-or 359  df-an 360  df-ex 1542

This theorem is used by: (None)