Theorem exp4b 632

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 633. (Revised by Wolf Lammen, 20-Jul-2021.)

Hypothesis

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

Assertion

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

Proof of Theorem exp4b

Step	Hyp	Ref	Expression
1		exp4b.1	. . 3 |- ( ( ph /\ ps ) -> ( ( ch /\ th ) -> ta ) )
2	1	expd 452	. 2 |- ( ( ph /\ ps ) -> ( ch -> ( th -> ta ) ) )
3	2	ex 450	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:  exp4a  633  exp43  640  somo  5069  tz7.7  5749  f1oweALT  7152  onfununi  7438  odi  7659  omeu  7665  nndi  7703  inf3lem2  8526  axdc3lem2  9273  genpnmax  9829  mulclprlem  9841  distrlem5pr  9849  reclem4pr  9872  lemul12a  10881  sup2  10979  nnmulcl  11043  zbtwnre  11786  elfz0fzfz0  12444  fzofzim  12514  fzo1fzo0n0  12518  elincfzoext  12525  elfzodifsumelfzo  12533  le2sq2  12939  expnbnd  12993  swrdswrd  13460  swrdccat3blem  13495  climbdd  14402  dvdslegcd  15226  oddprmgt2  15411  unbenlem  15612  infpnlem1  15614  prmgaplem6  15760  lmodvsdi  18886  lspsolvlem  19142  lbsextlem2  19159  gsummoncoe1  19674  cpmatmcllem  20523  mp2pm2mplem4  20614  1stccnp  21265  itg2le  23506  ewlkle  26501  clwlkclwwlklem2a  26899  3vfriswmgr  27142  frgrwopreg  27187  frgr2wwlk1  27193  frgrreg  27252  spansneleq  28429  elspansn4  28432  cvmdi  29183  atcvat3i  29255  mdsymlem3  29264  slmdvsdi  29768  mclsppslem  31480  dfon2lem8  31695  soseq  31751  heicant  33444  areacirclem1  33500  areacirclem2  33501  areacirclem4  33503  areacirc  33505  fzmul  33537  cvlexch1  34615  hlrelat2  34689  cvrat3  34728  snatpsubN  35036  pmaple  35047  fzopredsuc  41333  gbegt5  41649