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

Metamath Proof Explorer

Theorem 3orim123d

Description: Deduction joining 3 implications to form implication of disjunctions. (Contributed by NM, 4-Apr-1997)

Ref Expression
Hypotheses 3anim123d.1 ⊢ φ → ψ → χ
3anim123d.2 ⊢ φ → θ → τ
3anim123d.3 ⊢ φ → η → ζ
Assertion 3orim123d ⊢ φ → ψ ∨ θ ∨ η → χ ∨ τ ∨ ζ

Proof

Step Hyp Ref Expression
1 3anim123d.1 ⊢ φ → ψ → χ
2 3anim123d.2 ⊢ φ → θ → τ
3 3anim123d.3 ⊢ φ → η → ζ
4 1 2 orim12d ⊢ φ → ψ ∨ θ → χ ∨ τ
5 4 3 orim12d ⊢ φ → ψ ∨ θ ∨ η → χ ∨ τ ∨ ζ
6 df-3or ⊢ ψ ∨ θ ∨ η ↔ ψ ∨ θ ∨ η
7 df-3or ⊢ χ ∨ τ ∨ ζ ↔ χ ∨ τ ∨ ζ
8 5 6 7 3imtr4g ⊢ φ → ψ ∨ θ ∨ η → χ ∨ τ ∨ ζ