Theorem expd 420

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 419	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	com3r 88	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  expcomd  421  exp32  425  exp4b  435  exp4c  437  exp4d  438  exp42  440  exp44  442  exp5c  449  exp5j  450  exp5l  451  pm3.3  453  expdimp  457  impl  460  syland  614  mpan2d  706  a2and  858  3impib  1132  exp5o  1372  ralrimivv  3206  mob2  3681  reuind  3719  reupick3  4285  elpwunsn  4646  disjiun  5093  sotr2  5594  wefrc  5646  relop  5827  predpoirr  6324  predfrirr  6325  fnun  6639  mpteqb  6999  tpres  7189  fconst5  7194  funfvima  7218  riotaeqimp  7383  dfwe2  7761  limuni3  7836  tfisi  7843  trom  7859  funcnvuni  7917  resf1ext2b  7920  f1oweALT  7957  frxp  8110  poxp  8112  poxp2  8127  poxp3  8134  wfr3g  8304  onfununi  8316  tz7.48lem  8416  oecl  8510  oaordex  8531  oaass  8534  omwordri  8545  odi  8552  omass  8553  omeu  8558  oen0  8560  oewordi  8565  oewordri  8566  nnarcl  8590  nnmass  8598  brinxper  8712  findcard2  9137  rex2dom  9201  dif1ennnALT  9225  unblem1  9240  unblem2  9241  domunfican  9269  marypha1lem  9381  supiso  9424  inf3lem3  9587  epfrs  9688  frr3g  9716  karden  9869  infxpenlem  9985  iunfictbso  10086  dfac5  10100  dfac2b  10102  kmlem1  10122  kmlem9  10130  infpssrlem3  10277  fin23lem25  10296  fin23lem30  10314  domtriomlem  10414  axdc3lem4  10425  axcclem  10429  zorn2lem7  10474  konigthlem  10541  wunr1om  10692  tskr1om  10740  gruen  10785  grur1a  10792  indpi  10880  genpnmax  10980  prlem934  11006  ltaddpr  11007  ltexprlem7  11015  ltaprlem  11017  axrrecex  11136  axpre-sup  11142  lelttr  11288  dedekind  11361  addlid  11381  nn0lt2  12650  fzind  12685  fnn0ind  12686  btwnz  12690  uzwo  12926  lbzbi  12951  rpnnen1lem5  12996  ledivge1le  13080  xrlelttr  13172  qbtwnre  13216  xrsupsslem  13324  xrinfmsslem  13325  supxrun  13333  elfz1b  13612  elfz0ubfz0  13651  elfzo0z  13721  fzofzim  13729  elfznelfzo  13793  fleqceilz  13878  fsequb  14002  leexp2r  14201  bernneq  14256  fi1uzind  14534  brfi1indALT  14537  swrdnd0  14685  swrdswrdlem  14731  swrdswrd  14732  wrd2ind  14750  swrdccatin1  14752  swrdccatin2  14756  pfxccatin12lem3  14759  repswswrd  14811  cshweqrep  14848  swrd2lsw  14979  2swrd2eqwrdeq  14980  wrdl3s3  14989  s3iunsndisj  14995  cau3lem  15396  climuni  15593  mulcn2  15637  dvdsabseq  16361  divalglem8  16448  ndvdssub  16457  rplpwr  16606  algcvgblem  16625  lcmf  16681  lcmftp  16684  lcmfunsnlem2lem1  16686  lcmfunsnlem2lem2  16687  lcmfdvdsb  16691  lcmfun  16693  euclemma  16762  prmlem1a  17156  setsstruct2  17224  iscatd  17719  initoeu1  18058  initoeu2  18063  termoeu1  18065  plelttr  18388  insubm  18867  grpinveu  19031  cyccom  19265  symgfixelsi  19496  efgred  19809  telgsumfzs  20050  srgmulgass  20290  srgbinom  20304  lspdisjb  21219  mplcoe5lem  22150  cply1mul  22417  coe1fzgsumd  22425  gsummoncoe1  22429  evl1gsumd  22478  cpmatacl  22834  cpmatmcllem  22836  basis2  23069  0ntr  23189  uncmp  23521  1stcrest  23571  txcls  23722  txcnp  23738  tx1stc  23768  fgss2  23992  alexsubALTlem2  24166  alexsubALTlem3  24167  alexsubALTlem4  24168  metcnp3  24658  tngngp3  24774  reconn  24947  iscau4  25399  ellimc3  25999  ulmbdd  26519  ulmcn  26520  sinq12ge0  26631  gausslemma2dlem3  27490  2sq2  27555  2sqreultlem  27569  2sqreunnltlem  27572  sltsleft  28011  sltsright  28012  noseqind  28443  oldfib  28528  expsgt0  28588  bdayfinbndlem1  28618  bdayfin  28638  elreno2  28646  ax5seglem5  29192  ax5seg  29197  uhgrnbgr0nb  29613  cplgrop  29696  wlkl1loop  29896  uspgr2wlkeq  29904  upgrwlkdvdelem  29994  uhgrwkspthlem2  30012  pthdlem2lem  30025  uspgrn2crct  30066  wlkiswwlks2lem3  30129  wlkiswwlks2  30133  wlkiswwlksupgr2  30135  wlklnwwlkln2lem  30140  wwlksnext  30151  wwlksnextfun  30156  rusgrnumwwlk  30236  clwlkclwwlklem2a4  30257  clwlkclwwlklem3  30261  erclwwlksym  30281  erclwwlknsym  30330  eleclclwwlkn  30336  clwwlknonwwlknonb  30366  upgr3v3e3cycl  30440  upgr4cycl4dv4e  30445  conngrv2edg  30455  eupth2lem3lem6  30493  frgrncvvdeqlem8  30566  frgrwopreglem4a  30570  frgrreggt1  30653  frgrreg  30654  grpoinveu  30780  ococss  31554  shmodsi  31650  h1datomi  31842  hoaddsub  32077  adjmul  32353  chjatom  32618  atomli  32643  atcvat4i  32658  mdsymlem3  32666  mdsymlem5  32668  mdsymlem6  32669  sumdmdlem  32679  cdj3lem2a  32697  cdj3lem3a  32700  bnj1204  35317  fineqvinfep  35433  umgr2cycllem  35503  umgr2cycl  35504  cvmsdisj  35633  satfv0fun  35734  satffunlem  35764  satffunlem1lem2  35766  satffunlem2lem2  35769  fundmpss  36130  dfon2lem6  36149  dfon2lem8  36151  ifscgr  36407  lineext  36439  fscgr  36443  idinside  36447  btwnconn1lem11  36460  btwnconn1lem12  36461  btwnconn3  36466  brsegle  36471  seglecgr12  36474  hilbert1.2  36518  exp5d  36675  exp5k  36677  nn0prpwlem  36695  mh-inf3f1  36914  bj-restb  37596  exrecfnlem  37885  poimirlem26  38157  poimirlem29  38160  poimirlem32  38163  areacirc  38224  heibor1lem  38320  pridl  38548  pridlc  38582  dmnnzd  38586  disjlem17  39413  membpartlem19  39425  prtlem11  39502  prtlem17  39512  ax12indn  39579  atcvrj0  40064  cvrat4  40079  athgt  40092  lplnexllnN  40200  2llnjN  40203  lvolnle3at  40218  lncmp  40419  paddclN  40478  pexmidlem4N  40609  cdleme17d3  41132  cdleme50trn2  41187  cdlemf2  41198  cdlemf  41199  cdlemj3  41459  cdlemk26b-3  41541  dihord5b  41895  isnacs3  43303  jm2.26  43591  ordnexbtwnsuc  43856  omabs2  43921  naddgeoa  43983  sbiota1  45008  exbir  45053  tratrb  45110  onfrALT  45123  in2an  45182  pwtrrVD  45398  suctrALT2VD  45409  suctrALT2  45410  tratrbVD  45434  trintALTVD  45453  trintALT  45454  or2expropbi  47626  fcoresf1  47661  2reu8i  47705  2reuimp  47707  zm1nn  47894  2ffzoeq  47920  iccpartiltu  48026  iccpartigtl  48027  iccpartgt  48031  iccpartnel  48042  sbcpr  48125  fmtnofac2lem  48175  fmtnofac2  48176  lighneallem2  48213  odd2prm2  48338  stgoldbwt  48396  sbgoldbst  48398  sbgoldbaltlem1  48399  mogoldbb  48405  uhgrimisgrgric  48551  clnbgrgrim  48554  grimedg  48555  gpgedgvtx1  48682  gpgedg2iv  48687  pgnbgreunbgrlem3  48738  pgnbgreunbgrlem6  48744  pgnbgreunbgr  48745  lidldomn1  48851  ply1mulgsumlem1  49017  lincsumcl  49062  ellcoellss  49066  islinindfis  49080  lindslinindsimp1  49088  lindslinindsimp2lem5  49093  lindsrng01  49099  elfzolborelfzop1  49150  rrx2linest  49373  aacllem  50430