Metamath Proof Explorer


Theorem imp5g

Description: An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009)

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

Proof

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