Theorem exp43 640

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

Hypothesis

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

Assertion

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

Proof of Theorem exp43

Step	Hyp	Ref	Expression
1		exp43.1	. . 3 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
2	1	ex 450	. 2 |- ( ( ph /\ ps ) -> ( ( ch /\ th ) -> ta ) )
3	2	exp4b 632	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:  exp53  647  funssres  5930  fvopab3ig  6278  fvmptt  6300  fvn0elsuppb  7312  tfr3  7495  omordi  7646  odi  7659  nnmordi  7711  php  8144  fiint  8237  ordiso2  8420  cfcoflem  9094  zorn2lem5  9322  inar1  9597  psslinpr  9853  recexsrlem  9924  qaddcl  11804  qmulcl  11806  elfznelfzo  12573  expcan  12913  ltexp2  12914  bernneq  12990  expnbnd  12993  relexpaddg  13793  lcmfunsnlem2lem1  15351  initoeu2lem1  16664  elcls3  20887  opnneissb  20918  txbas  21370  grpoidinvlem3  27360  grporcan  27372  shscli  28176  spansncol  28427  spanunsni  28438  spansncvi  28511  homco1  28660  homulass  28661  atomli  29241  chirredlem1  29249  cdj1i  29292  frinfm  33530  filbcmb  33535  unichnidl  33830  dmncan1  33875  pclfinclN  35236  iccelpart  41369  prmdvdsfmtnof1lem2  41497  scmsuppss  42153