Theorem exp44 611

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

Hypothesis

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

Assertion

Ref	Expression
exp44	|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Proof of Theorem exp44

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

Syntax hints:   -> wi 4   /\ wa 367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 369

This theorem is referenced by:  wefrc  4862  tz7.7  4893  oalimcl  7201  unbenlem  14510  rnelfm  20620  wwlknimp  24889  spansncvi  26768  atom1d  27470  chirredlem3  27509  finminlem  30376  cvlcvr1  35461  lhpexle2lem  36130  trlord  36692  cdlemkid4  37057  dihord6apre  37380  dihglbcpreN  37424