Metamath Proof Explorer


Theorem exp4c

Description: An exportation inference. (Contributed by NM, 26-Apr-1994)

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

Proof

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