Theorem expd 415

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  expcomd  416  exp32  420  exp4b  430  exp4c  432  exp4d  433  exp42  435  exp44  437  exp5c  444  exp5j  445  exp5l  446  pm3.3  448  expdimp  452  impl  455  syland  604  mpan2d  695  a2and  846  3impib  1117  exp5o  1357  ralrimivv  3179  mob2  3662  reuind  3700  reupick3  4271  elpwunsn  4629  disjiun  5074  sotr2  5566  wefrc  5618  relop  5799  predpoirr  6291  predfrirr  6292  fnun  6606  mpteqb  6961  tpres  7149  fconst5  7154  funfvima  7178  riotaeqimp  7343  dfwe2  7721  limuni3  7796  tfisi  7803  trom  7819  funcnvuni  7876  resf1ext2b  7879  f1oweALT  7918  frxp  8069  poxp  8071  poxp2  8086  poxp3  8093  wfr3g  8262  onfununi  8274  tz7.48lem  8373  oecl  8465  oaordex  8486  oaass  8489  omwordri  8500  odi  8507  omass  8508  omeu  8513  oen0  8515  oewordi  8520  oewordri  8521  nnarcl  8545  nnmass  8553  brinxper  8666  findcard2  9092  rex2dom  9156  dif1ennnALT  9180  unblem1  9195  unblem2  9196  domunfican  9225  marypha1lem  9339  supiso  9382  inf3lem3  9542  epfrs  9643  frr3g  9671  karden  9810  infxpenlem  9926  iunfictbso  10027  dfac5  10042  dfac2b  10044  kmlem1  10064  kmlem9  10072  infpssrlem3  10218  fin23lem25  10237  fin23lem30  10255  domtriomlem  10355  axdc3lem4  10366  axcclem  10370  zorn2lem7  10415  konigthlem  10482  wunr1om  10633  tskr1om  10681  gruen  10726  grur1a  10733  indpi  10821  genpnmax  10921  prlem934  10947  ltaddpr  10948  ltexprlem7  10956  ltaprlem  10958  axrrecex  11077  axpre-sup  11083  lelttr  11227  dedekind  11300  addlid  11320  nn0lt2  12583  fzind  12618  fnn0ind  12619  btwnz  12623  uzwo  12852  lbzbi  12877  rpnnen1lem5  12922  ledivge1le  13006  xrlelttr  13098  qbtwnre  13142  xrsupsslem  13250  xrinfmsslem  13251  supxrun  13259  elfz1b  13538  elfz0ubfz0  13577  elfzo0z  13647  fzofzim  13655  elfznelfzo  13719  fleqceilz  13804  fsequb  13928  leexp2r  14127  bernneq  14182  fi1uzind  14460  brfi1indALT  14463  swrdnd0  14611  swrdswrdlem  14657  swrdswrd  14658  wrd2ind  14676  swrdccatin1  14678  swrdccatin2  14682  pfxccatin12lem3  14685  repswswrd  14737  cshweqrep  14774  swrd2lsw  14905  2swrd2eqwrdeq  14906  wrdl3s3  14915  s3iunsndisj  14921  cau3lem  15308  climuni  15505  mulcn2  15549  dvdsabseq  16273  divalglem8  16360  ndvdssub  16369  rplpwr  16518  algcvgblem  16537  lcmf  16593  lcmftp  16596  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfdvdsb  16603  lcmfun  16605  euclemma  16674  prmlem1a  17068  setsstruct2  17135  iscatd  17630  initoeu1  17969  initoeu2  17974  termoeu1  17976  plelttr  18299  insubm  18777  grpinveu  18941  cyccom  19169  symgfixelsi  19401  efgred  19714  telgsumfzs  19955  srgmulgass  20189  srgbinom  20203  lspdisjb  21116  mplcoe5lem  22027  cply1mul  22271  coe1fzgsumd  22279  gsummoncoe1  22283  evl1gsumd  22332  cpmatacl  22691  cpmatmcllem  22693  basis2  22926  0ntr  23046  uncmp  23378  1stcrest  23428  txcls  23579  txcnp  23595  tx1stc  23625  fgss2  23849  alexsubALTlem2  24023  alexsubALTlem3  24024  alexsubALTlem4  24025  metcnp3  24515  tngngp3  24631  reconn  24804  iscau4  25256  ellimc3  25856  ulmbdd  26376  ulmcn  26377  sinq12ge0  26485  gausslemma2dlem3  27345  2sq2  27410  2sqreultlem  27424  2sqreunnltlem  27427  sltsleft  27866  sltsright  27867  noseqind  28298  oldfib  28383  expsgt0  28443  bdayfinbndlem1  28473  bdayfin  28493  elreno2  28501  ax5seglem5  29016  ax5seg  29021  uhgrnbgr0nb  29437  cplgrop  29520  wlkl1loop  29721  uspgr2wlkeq  29729  upgrwlkdvdelem  29819  uhgrwkspthlem2  29837  pthdlem2lem  29850  uspgrn2crct  29891  wlkiswwlks2lem3  29954  wlkiswwlks2  29958  wlkiswwlksupgr2  29960  wlklnwwlkln2lem  29965  wwlksnext  29976  wwlksnextfun  29981  rusgrnumwwlk  30061  clwlkclwwlklem2a4  30082  clwlkclwwlklem3  30086  erclwwlksym  30106  erclwwlknsym  30155  eleclclwwlkn  30161  clwwlknonwwlknonb  30191  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  conngrv2edg  30280  eupth2lem3lem6  30318  frgrncvvdeqlem8  30391  frgrwopreglem4a  30395  frgrreggt1  30478  frgrreg  30479  grpoinveu  30605  ococss  31379  shmodsi  31475  h1datomi  31667  hoaddsub  31902  adjmul  32178  chjatom  32443  atomli  32468  atcvat4i  32483  mdsymlem3  32491  mdsymlem5  32493  mdsymlem6  32494  sumdmdlem  32504  cdj3lem2a  32522  cdj3lem3a  32525  bnj1204  35170  fineqvinfep  35285  umgr2cycllem  35338  umgr2cycl  35339  cvmsdisj  35468  satfv0fun  35569  satffunlem  35599  satffunlem1lem2  35601  satffunlem2lem2  35604  fundmpss  35965  dfon2lem6  35984  dfon2lem8  35986  ifscgr  36242  lineext  36274  fscgr  36278  idinside  36282  btwnconn1lem11  36295  btwnconn1lem12  36296  btwnconn3  36301  brsegle  36306  seglecgr12  36309  hilbert1.2  36353  exp5d  36500  exp5k  36502  nn0prpwlem  36520  mh-inf3f1  36739  bj-restb  37422  exrecfnlem  37709  poimirlem26  37981  poimirlem29  37984  poimirlem32  37987  areacirc  38048  heibor1lem  38144  pridl  38372  pridlc  38406  dmnnzd  38410  disjlem17  39237  membpartlem19  39249  prtlem11  39326  prtlem17  39336  ax12indn  39403  atcvrj0  39888  cvrat4  39903  athgt  39916  lplnexllnN  40024  2llnjN  40027  lvolnle3at  40042  lncmp  40243  paddclN  40302  pexmidlem4N  40433  cdleme17d3  40956  cdleme50trn2  41011  cdlemf2  41022  cdlemf  41023  cdlemj3  41283  cdlemk26b-3  41365  dihord5b  41719  isnacs3  43156  jm2.26  43448  ordnexbtwnsuc  43713  omabs2  43778  naddgeoa  43840  sbiota1  44879  exbir  44924  tratrb  44981  onfrALT  44994  in2an  45053  pwtrrVD  45269  suctrALT2VD  45280  suctrALT2  45281  tratrbVD  45305  trintALTVD  45324  trintALT  45325  or2expropbi  47494  fcoresf1  47529  2reu8i  47573  2reuimp  47575  zm1nn  47762  2ffzoeq  47788  iccpartiltu  47894  iccpartigtl  47895  iccpartgt  47899  iccpartnel  47910  sbcpr  47993  fmtnofac2lem  48043  fmtnofac2  48044  lighneallem2  48081  odd2prm2  48206  stgoldbwt  48264  sbgoldbst  48266  sbgoldbaltlem1  48267  mogoldbb  48273  uhgrimisgrgric  48419  clnbgrgrim  48422  grimedg  48423  gpgedgvtx1  48550  gpgedg2iv  48555  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem6  48612  pgnbgreunbgr  48613  lidldomn1  48719  ply1mulgsumlem1  48874  lincsumcl  48919  ellcoellss  48923  islinindfis  48937  lindslinindsimp1  48945  lindslinindsimp2lem5  48950  lindsrng01  48956  elfzolborelfzop1  49007  rrx2linest  49230  aacllem  50288