Metamath Proof Explorer


Theorem exp512

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

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

Proof

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