Theorem 19.34 1663

Description: Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
19.34	⊢ ((∀xφ ∨ ∃xψ) → ∃x(φ ∨ ψ))

Proof of Theorem 19.34

Step	Hyp	Ref	Expression
1		19.2 1659	. . 3 ⊢ (∀xφ → ∃xφ)
2	1	orim1i 503	. 2 ⊢ ((∀xφ ∨ ∃xψ) → (∃xφ ∨ ∃xψ))
3		19.43 1605	. 2 ⊢ (∃x(φ ∨ ψ) ↔ (∃xφ ∨ ∃xψ))
4	2, 3	sylibr 203	1 ⊢ ((∀xφ ∨ ∃xψ) → ∃x(φ ∨ ψ))

This proof depends on syntax axioms:   → wi 4   ∨ wo 357  ∀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  ax-9 1654

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

This theorem is used by: (None)