Metamath Proof Explorer

Theorem imp5p

Description: A triple importation inference. (Contributed by Jeff Hankins, 8-Jul-2009)

Ref Expression
Hypothesis 3imp5.1 ⊢ φ → ψ → χ → θ → τ → η
Assertion imp5p ⊢ φ → ψ → χ ∧ θ ∧ τ → η

Proof

Step Hyp Ref Expression
1 3imp5.1 ⊢ φ → ψ → χ → θ → τ → η
2 1 com52l ⊢ χ → θ → τ → φ → ψ → η
3 2 3imp ⊢ χ ∧ θ ∧ τ → φ → ψ → η
4 3 com3l ⊢ φ → ψ → χ ∧ θ ∧ τ → η