Metamath Proof Explorer


Theorem exp510

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

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

Proof

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