Theorem exp44 613

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 605	. 2 |- ( ph -> ( ( ps /\ ch ) -> ( th -> ta ) ) )
3	2	expd 436	1 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Syntax hints:   -> wi 4   /\ wa 369

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 371

This theorem is referenced by:  wefrc  4825  tz7.7  4856  oalimcl  7112  unbenlem  14090  rnelfm  19661  spansncvi  25227  atom1d  25929  chirredlem3  25968  finminlem  28681  wwlknimp  30489  cvlcvr1  33342  lhpexle2lem  34011  trlord  34571  cdlemkid4  34936  dihord6apre  35259  dihglbcpreN  35303