Metamath Proof Explorer


Theorem exp5g

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

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

Proof

Step Hyp Ref Expression
1 exp5g.1 φ ψ χ θ τ η
2 1 exp4c φ ψ χ θ τ η
3 2 ex φ ψ χ θ τ η