Theorem ecase23d 1285

Description: Deduction for elimination by cases. (Contributed by NM, 22-Apr-1994.)

Hypotheses

Ref	Expression
ecase23d.1	⊢ (φ → ¬ χ)
ecase23d.2	⊢ (φ → ¬ θ)
ecase23d.3	⊢ (φ → (ψ ∨ χ ∨ θ))

Assertion

Ref	Expression
ecase23d	⊢ (φ → ψ)

Proof of Theorem ecase23d

Step	Hyp	Ref	Expression
1		ecase23d.1	. . 3 ⊢ (φ → ¬ χ)
2		ecase23d.2	. . 3 ⊢ (φ → ¬ θ)
3		ioran 476	. . 3 ⊢ (¬ (χ ∨ θ) ↔ (¬ χ ∧ ¬ θ))
4	1, 2, 3	sylanbrc 645	. 2 ⊢ (φ → ¬ (χ ∨ θ))
5		ecase23d.3	. . . 4 ⊢ (φ → (ψ ∨ χ ∨ θ))
6		3orass 937	. . . 4 ⊢ ((ψ ∨ χ ∨ θ) ↔ (ψ ∨ (χ ∨ θ)))
7	5, 6	sylib 188	. . 3 ⊢ (φ → (ψ ∨ (χ ∨ θ)))
8	7	ord 366	. 2 ⊢ (φ → (¬ ψ → (χ ∨ θ)))
9	4, 8	mt3d 117	1 ⊢ (φ → ψ)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 357   ∨ w3o 933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935

This theorem is referenced by:  tfinltfin  4502