Theorem exp45 642

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

Hypothesis

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

Assertion

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

Proof of Theorem exp45

Step	Hyp	Ref	Expression
1		exp45.1	. . 3 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ta )
2	1	exp32 631	. 2 |- ( ph -> ( ps -> ( ( ch /\ th ) -> ta ) ) )
3	2	exp4a 633	1 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  oaass  7641  zorn2lem4  9321  zorn2lem7  9324  iscatd2  16342  fgss2  21678  alexsubALTlem4  21854  grporcan  27372  spansncvi  28511  mdsymlem5  29266  riotasv3d  34246  cvratlem  34707  hbtlem2  37694