Metamath Proof Explorer


Theorem exp5l

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

Ref Expression
Hypothesis exp5l.1
|- ( ph -> ( ( ( ps /\ ch ) /\ ( th /\ ta ) ) -> et ) )
Assertion exp5l
|- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )

Proof

Step Hyp Ref Expression
1 exp5l.1
 |-  ( ph -> ( ( ( ps /\ ch ) /\ ( th /\ ta ) ) -> et ) )
2 1 expd
 |-  ( ph -> ( ( ps /\ ch ) -> ( ( th /\ ta ) -> et ) ) )
3 2 exp5c
 |-  ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) )