Theorem exp4a 633

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2021.)

Hypothesis

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

Assertion

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

Proof of Theorem exp4a

Step	Hyp	Ref	Expression
1		exp4a.1	. . 3 |- ( ph -> ( ps -> ( ( ch /\ th ) -> ta ) ) )
2	1	imp 445	. 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:  exp4bOLD  635  exp4d  637  exp45  642  exp5c  644  tz7.7  5749  wfrlem12  7426  tfr3  7495  oaass  7641  omordi  7646  nnmordi  7711  fiint  8237  zorn2lem6  9323  zorn2lem7  9324  mulgt0sr  9926  sqlecan  12971  rexuzre  14092  caurcvg  14407  ndvdssub  15133  lsmcv  19141  iscnp4  21067  nrmsep3  21159  2ndcdisj  21259  2ndcsep  21262  tsmsxp  21958  metcnp3  22345  xrlimcnp  24695  ax5seglem5  25813  elspansn4  28432  hoadddir  28663  atcvatlem  29244  sumdmdii  29274  sumdmdlem  29277  frrlem11  31792  isbasisrelowllem1  33203  isbasisrelowllem2  33204  prtlem17  34161  cvratlem  34707  athgt  34742  lplnnle2at  34827  lplncvrlvol2  34901  cdlemb  35080  dalaw  35172  cdleme50trn2  35839  cdlemg18b  35967  dihmeetlem3N  36594  onfrALTlem2  38761  in3an  38836  lindslinindsimp1  42246