Metamath Proof Explorer


Theorem imp5q

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

Ref Expression
Hypothesis 3imp5.1 φ ψ χ θ τ η
Assertion imp5q φ ψ χ θ τ η

Proof

Step Hyp Ref Expression
1 3imp5.1 φ ψ χ θ τ η
2 1 imp φ ψ χ θ τ η
3 2 3impd φ ψ χ θ τ η