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  603  mpan2d  694  a2and  845  3impib  1116  exp5o  1355  ralrimivv  3199  mob2  3720  reuind  3758  reupick3  4329  elpwunsn  4683  disjiun  5130  sotr2  5625  wefrc  5678  relop  5860  predpoirr  6353  predfrirr  6354  fnun  6681  mpteqb  7034  tpres  7222  fconst5  7227  funfvima  7251  riotaeqimp  7415  dfwe2  7795  limuni3  7874  tfisi  7881  trom  7897  funcnvuni  7955  resf1ext2b  7958  f1oweALT  7998  frxp  8152  poxp  8154  poxp2  8169  poxp3  8176  wfr3g  8348  wfrlem12OLD  8361  onfununi  8382  tz7.48lem  8482  oecl  8576  oaordex  8597  oaass  8600  omwordri  8611  odi  8618  omass  8619  omeu  8624  oen0  8625  oewordi  8630  oewordri  8631  nnarcl  8655  nnmass  8663  brinxper  8775  findcard2  9205  rex2dom  9283  dif1ennnALT  9312  unblem1  9329  unblem2  9330  domunfican  9362  marypha1lem  9474  supiso  9516  inf3lem3  9671  epfrs  9772  frr3g  9797  karden  9936  infxpenlem  10054  iunfictbso  10155  dfac5  10170  dfac2b  10172  kmlem1  10192  kmlem9  10200  infpssrlem3  10346  fin23lem25  10365  fin23lem30  10383  domtriomlem  10483  axdc3lem4  10494  axcclem  10498  zorn2lem7  10543  konigthlem  10609  wunr1om  10760  tskr1om  10808  gruen  10853  grur1a  10860  indpi  10948  genpnmax  11048  prlem934  11074  ltaddpr  11075  ltexprlem7  11083  ltaprlem  11085  axrrecex  11204  axpre-sup  11210  lelttr  11352  dedekind  11425  addlid  11445  nn0lt2  12683  fzind  12718  fnn0ind  12719  btwnz  12723  uzwo  12954  lbzbi  12979  rpnnen1lem5  13024  ledivge1le  13107  xrlelttr  13199  qbtwnre  13242  xrsupsslem  13350  xrinfmsslem  13351  supxrun  13359  elfz1b  13634  elfz0ubfz0  13673  elfzo0z  13742  fzofzim  13750  elfznelfzo  13812  fleqceilz  13895  fsequb  14017  leexp2r  14215  bernneq  14269  fi1uzind  14547  brfi1indALT  14550  swrdnd0  14696  swrdswrdlem  14743  swrdswrd  14744  wrd2ind  14762  swrdccatin1  14764  swrdccatin2  14768  pfxccatin12lem3  14771  repswswrd  14823  cshweqrep  14860  swrd2lsw  14992  2swrd2eqwrdeq  14993  wrdl3s3  15002  s3iunsndisj  15008  cau3lem  15394  climuni  15589  mulcn2  15633  dvdsabseq  16351  divalglem8  16438  ndvdssub  16447  rplpwr  16596  algcvgblem  16615  lcmf  16671  lcmftp  16674  lcmfunsnlem2lem1  16676  lcmfunsnlem2lem2  16677  lcmfdvdsb  16681  lcmfun  16683  euclemma  16751  prmlem1a  17145  setsstruct2  17212  iscatd  17717  initoeu1  18057  initoeu2  18062  termoeu1  18064  plelttr  18390  insubm  18832  grpinveu  18993  cyccom  19222  symgfixelsi  19454  efgred  19767  telgsumfzs  20008  srgmulgass  20215  srgbinom  20229  lspdisjb  21129  mplcoe5lem  22058  cply1mul  22301  coe1fzgsumd  22309  gsummoncoe1  22313  evl1gsumd  22362  cpmatacl  22723  cpmatmcllem  22725  basis2  22959  0ntr  23080  uncmp  23412  1stcrest  23462  txcls  23613  txcnp  23629  tx1stc  23659  fgss2  23883  alexsubALTlem2  24057  alexsubALTlem3  24058  alexsubALTlem4  24059  metcnp3  24554  tngngp3  24678  reconn  24851  iscau4  25314  ellimc3  25915  ulmbdd  26442  ulmcn  26443  sinq12ge0  26551  gausslemma2dlem3  27413  2sq2  27478  2sqreultlem  27492  2sqreunnltlem  27495  ssltleft  27910  ssltright  27911  noseqind  28299  expsgt0  28416  ax5seglem5  28949  ax5seg  28954  uhgrnbgr0nb  29372  cplgrop  29455  wlkl1loop  29657  uspgr2wlkeq  29665  upgrwlkdvdelem  29757  uhgrwkspthlem2  29775  pthdlem2lem  29788  uspgrn2crct  29829  wlkiswwlks2lem3  29892  wlkiswwlks2  29896  wlkiswwlksupgr2  29898  wlklnwwlkln2lem  29903  wwlksnext  29914  wwlksnextfun  29919  rusgrnumwwlk  29996  clwlkclwwlklem2a4  30017  clwlkclwwlklem3  30021  erclwwlksym  30041  erclwwlknsym  30090  eleclclwwlkn  30096  clwwlknonwwlknonb  30126  upgr3v3e3cycl  30200  upgr4cycl4dv4e  30205  conngrv2edg  30215  eupth2lem3lem6  30253  frgrncvvdeqlem8  30326  frgrwopreglem4a  30330  frgrreggt1  30413  frgrreg  30414  grpoinveu  30539  ococss  31313  shmodsi  31409  h1datomi  31601  hoaddsub  31836  adjmul  32112  chjatom  32377  atomli  32402  atcvat4i  32417  mdsymlem3  32425  mdsymlem5  32427  mdsymlem6  32428  sumdmdlem  32438  cdj3lem2a  32456  cdj3lem3a  32459  bnj1204  35027  umgr2cycllem  35146  umgr2cycl  35147  cvmsdisj  35276  satfv0fun  35377  satffunlem  35407  satffunlem1lem2  35409  satffunlem2lem2  35412  fundmpss  35768  dfon2lem6  35790  dfon2lem8  35792  ifscgr  36046  lineext  36078  fscgr  36082  idinside  36086  btwnconn1lem11  36099  btwnconn1lem12  36100  btwnconn3  36105  brsegle  36110  seglecgr12  36113  hilbert1.2  36157  exp5d  36304  exp5k  36306  nn0prpwlem  36324  bj-restb  37096  exrecfnlem  37381  poimirlem26  37654  poimirlem29  37657  poimirlem32  37660  areacirc  37721  heibor1lem  37817  pridl  38045  pridlc  38079  dmnnzd  38083  disjlem17  38801  membpartlem19  38813  prtlem11  38868  prtlem17  38878  ax12indn  38945  atcvrj0  39431  cvrat4  39446  athgt  39459  lplnexllnN  39567  2llnjN  39570  lvolnle3at  39585  lncmp  39786  paddclN  39845  pexmidlem4N  39976  cdleme17d3  40499  cdleme50trn2  40554  cdlemf2  40565  cdlemf  40566  cdlemj3  40826  cdlemk26b-3  40908  dihord5b  41262  isnacs3  42726  jm2.26  43019  ordnexbtwnsuc  43285  omabs2  43350  naddgeoa  43412  sbiota1  44458  exbir  44504  tratrb  44561  onfrALT  44574  in2an  44633  pwtrrVD  44850  suctrALT2VD  44861  suctrALT2  44862  tratrbVD  44886  trintALTVD  44905  trintALT  44906  or2expropbi  47051  fcoresf1  47086  2reu8i  47130  2reuimp  47132  zm1nn  47319  2ffzoeq  47344  iccpartiltu  47414  iccpartigtl  47415  iccpartgt  47419  iccpartnel  47430  sbcpr  47513  fmtnofac2lem  47560  fmtnofac2  47561  lighneallem2  47598  odd2prm2  47710  stgoldbwt  47768  sbgoldbst  47770  sbgoldbaltlem1  47771  mogoldbb  47777  uhgrimisgrgric  47904  clnbgrgrim  47907  grimedg  47908  gpgedgvtx1  48025  lidldomn1  48152  ply1mulgsumlem1  48308  lincsumcl  48353  ellcoellss  48357  islinindfis  48371  lindslinindsimp1  48379  lindslinindsimp2lem5  48384  lindsrng01  48390  elfzolborelfzop1  48441  rrx2linest  48668  aacllem  49375