Theorem expd 421

Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 28-Jul-2022.)

Hypothesis

Ref	Expression
expd.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
expd	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem expd

Step	Hyp	Ref	Expression
1		expd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expdcom 420	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	com3r 88	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  expcomd  422  exp32  426  exp4b  436  exp4c  438  exp4d  439  exp42  441  exp44  443  exp5c  450  exp5j  451  exp5l  452  pm3.3  454  expdimp  458  impl  461  syland  615  mpan2d  707  a2and  859  3impib  1134  exp5o  1374  ralrimivv  3203  mob2  3673  reuind  3711  reupick3  4276  elpwunsn  4645  disjiun  5091  sotr2  5597  wefrc  5649  relop  5830  predpoirr  6331  predfrirr  6332  fnun  6646  mpteqb  7006  tpres  7200  fconst5  7205  funfvima  7229  riotaeqimp  7396  dfwe2  7773  limuni3  7848  tfisi  7855  trom  7871  funcnvuni  7929  resf1ext2b  7932  f1oweALT  7969  frxp  8124  poxp  8126  poxp2  8141  poxp3  8148  wfr3g  8318  onfununi  8330  tz7.48lem  8430  oecl  8524  oaordex  8545  oaass  8548  omwordri  8559  odi  8566  omass  8567  omeu  8572  oen0  8574  oewordi  8579  oewordri  8580  nnarcl  8604  nnmass  8612  brinxper  8726  findcard2  9159  rex2dom  9223  dif1ennnALT  9247  unblem1  9262  unblem2  9263  domunfican  9291  marypha1lem  9403  supiso  9446  inf3lem3  9609  epfrs  9710  frr3g  9738  kardenOLD  9899  infxpenlem  10016  iunfictbso  10117  dfac5  10131  dfac2b  10133  kmlem1  10153  kmlem9  10161  infpssrlem3  10307  fin23lem25  10326  fin23lem30  10344  domtriomlem  10444  axdc3lem4  10455  axcclem  10459  zorn2lem7  10504  konigthlem  10577  wunr1om  10728  tskr1om  10776  gruen  10821  grur1a  10828  indpi  10916  genpnmax  11016  prlem934  11042  ltaddpr  11043  ltexprlem7  11051  ltaprlem  11053  axrrecex  11172  axpre-sup  11178  lelttr  11324  dedekind  11397  addlid  11417  nn0lt2  12684  fzind  12719  fnn0ind  12720  btwnz  12724  uzwo  12960  lbzbi  12985  rpnnen1lem5  13031  ledivge1le  13115  xrlelttr  13207  qbtwnre  13251  xrsupsslem  13359  xrinfmsslem  13360  supxrun  13368  elfz1b  13648  elfz0ubfz0  13687  elfzo0z  13757  fzofzim  13765  elfznelfzo  13829  fleqceilz  13915  fsequb  14039  leexp2r  14238  bernneq  14293  fi1uzind  14572  brfi1indALT  14575  swrdnd0  14727  swrdswrdlem  14773  swrdswrd  14774  wrd2ind  14792  swrdccatin1  14794  swrdccatin2  14798  pfxccatin12lem3  14801  repswswrd  14855  cshweqrep  14892  swrd2lsw  15025  2swrd2eqwrdeq  15026  wrdl3s3  15035  s3iunsndisj  15041  cau3lem  15442  climuni  15639  mulcn2  15683  dvdsabseq  16403  divalglem8  16490  ndvdssub  16499  rplpwr  16648  algcvgblem  16667  lcmf  16723  lcmftp  16726  lcmfunsnlem2lem1  16728  lcmfunsnlem2lem2  16729  lcmfdvdsb  16733  lcmfun  16735  euclemma  16804  prmlem1a  17198  setsstruct2  17266  iscatd  17761  initoeu1  18100  initoeu2  18105  termoeu1  18107  plelttr  18430  insubm  18927  grpinveu  19098  cyccom  19331  symgfixelsi  19562  efgred  19875  telgsumfzs  20116  srgmulgass  20356  srgbinom  20370  lspdisjb  21313  mplcoe5lem  22255  cply1mul  22521  coe1fzgsumd  22529  gsummoncoe1  22533  evl1gsumd  22582  cpmatacl  22941  cpmatmcllem  22943  basis2  23176  0ntr  23296  uncmp  23628  1stcrest  23678  txcls  23830  txcnp  23846  tx1stc  23876  fgss2  24100  alexsubALTlem2  24274  alexsubALTlem3  24275  alexsubALTlem4  24276  metcnp3  24766  tngngp3  24882  reconn  25055  iscau4  25507  ellimc3  26106  ulmbdd  26634  ulmcn  26635  sinq12ge0  26746  gausslemma2dlem3  27604  2sq2  27669  2sqreultlem  27683  2sqreunnltlem  27686  sltsleft  28125  sltsright  28126  noseqind  28557  oldfib  28642  expsgt0  28702  bdayfinbndlem1  28732  bdayfin  28752  elreno2  28760  ax5seglem5  29390  ax5seg  29395  uhgrnbgr0nb  29814  cplgrop  29897  wlkl1loop  30097  uspgr2wlkeq  30105  upgrwlkdvdelem  30201  uhgrwkspthlem2  30219  pthdlem2lem  30232  uspgrn2crct  30276  wlkiswwlks2lem3  30339  wlkiswwlks2  30343  wlkiswwlksupgr2  30345  wlklnwwlkln2lem  30350  wwlksnext  30361  wwlksnextfun  30366  rusgrnumwwlk  30446  clwlkclwwlklem2a4  30467  clwlkclwwlklem3  30471  erclwwlksym  30491  erclwwlknsym  30540  eleclclwwlkn  30546  clwwlknonwwlknonb  30576  umgr2cycllem  30625  umgr2cycl  30626  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  conngrv2edg  30675  eupth2lem3lem6  30713  frgrncvvdeqlem8  30786  frgrwopreglem4a  30790  frgrreggt1  30873  frgrreg  30874  grpoinveu  31000  ococss  31774  shmodsi  31870  h1datomi  32062  hoaddsub  32297  adjmul  32573  chjatom  32838  atomli  32863  atcvat4i  32878  mdsymlem3  32886  mdsymlem5  32888  mdsymlem6  32889  sumdmdlem  32899  cdj3lem2a  32917  cdj3lem3a  32920  bnj1204  35521  fineqvinfep  35651  cvmsdisj  35849  satfv0fun  35950  satffunlem  35980  satffunlem1lem2  35982  satffunlem2lem2  35985  fundmpss  36346  dfon2lem6  36365  dfon2lem8  36367  ifscgr  36624  lineext  36656  fscgr  36660  idinside  36664  btwnconn1lem11  36677  btwnconn1lem12  36678  btwnconn3  36683  brsegle  36688  seglecgr12  36691  hilbert1.2  36735  exp5d  36922  exp5k  36924  nn0prpwlem  36941  mh-inf3f1  37160  bj-restb  37844  exrecfnlem  38133  poimirlem26  38395  poimirlem29  38398  poimirlem32  38401  areacirc  38462  heibor1lem  38559  pridl  38787  pridlc  38821  dmnnzd  38825  disjlem17  39650  membpartlem19  39662  prtlem11  39739  prtlem17  39749  ax12indn  39816  atcvrj0  40301  cvrat4  40316  athgt  40329  lplnexllnN  40437  2llnjN  40440  lvolnle3at  40455  lncmp  40656  paddclN  40715  pexmidlem4N  40846  cdleme17d3  41369  cdleme50trn2  41424  cdlemf2  41435  cdlemf  41436  cdlemj3  41696  cdlemk26b-3  41778  dihord5b  42132  isnacs3  43555  jm2.26  43843  ordnexbtwnsuc  44108  omabs2  44173  naddgeoa  44235  sbiota1  45258  exbir  45302  tratrb  45359  onfrALT  45372  in2an  45431  pwtrrVD  45647  suctrALT2VD  45658  suctrALT2  45659  tratrbVD  45683  trintALTVD  45702  trintALT  45703  or2expropbi  47922  fcoresf1  47957  2reu8i  48001  2reuimp  48003  zm1nn  48190  2ffzoeq  48216  iccpartiltu  48322  iccpartigtl  48323  iccpartgt  48327  iccpartnel  48338  sbcpr  48421  fmtnofac2lem  48471  fmtnofac2  48472  lighneallem2  48509  odd2prm2  48634  stgoldbwt  48692  sbgoldbst  48694  sbgoldbaltlem1  48695  mogoldbb  48701  uhgrimisgrgric  48847  clnbgrgrim  48850  grimedg  48851  gpgedgvtx1  48978  gpgedg2iv  48983  pgnbgreunbgrlem3  49034  pgnbgreunbgrlem6  49040  pgnbgreunbgr  49041  lidldomn1  49146  idomnzd  49261  ply1mulgsumlem1  49316  lincsumcl  49361  ellcoellss  49365  islinindfis  49379  lindslinindsimp1  49387  lindslinindsimp2lem5  49392  lindsrng01  49398  elfzolborelfzop1  49449  rrx2linest  49672  aacllem  50772