Metamath Proof Explorer


Theorem exp5l

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

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

Proof

Step Hyp Ref Expression
1 exp5l.1 φψχθτη
2 1 expd φψχθτη
3 2 exp5c φψχθτη