Metamath Proof Explorer

Theorem 3jaodd

Description: Double deduction form of 3jaoi . (Contributed by Scott Fenton, 20-Apr-2011)

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

Proof

Step Hyp Ref Expression
1 3jaodd.1 ⊢ φ → ψ → χ → η
2 3jaodd.2 ⊢ φ → ψ → θ → η
3 3jaodd.3 ⊢ φ → ψ → τ → η
4 1 com3r ⊢ χ → φ → ψ → η
5 2 com3r ⊢ θ → φ → ψ → η
6 3 com3r ⊢ τ → φ → ψ → η
7 4 5 6 3jaoi ⊢ χ ∨ θ ∨ τ → φ → ψ → η
8 7 com3l ⊢ φ → ψ → χ ∨ θ ∨ τ → η