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  3178  mob2  3661  reuind  3699  reupick3  4270  elpwunsn  4628  disjiun  5073  sotr2  5573  wefrc  5625  relop  5805  predpoirr  6297  predfrirr  6298  fnun  6612  mpteqb  6967  tpres  7156  fconst5  7161  funfvima  7185  riotaeqimp  7350  dfwe2  7728  limuni3  7803  tfisi  7810  trom  7826  funcnvuni  7883  resf1ext2b  7886  f1oweALT  7925  frxp  8076  poxp  8078  poxp2  8093  poxp3  8100  wfr3g  8269  onfununi  8281  tz7.48lem  8380  oecl  8472  oaordex  8493  oaass  8496  omwordri  8507  odi  8514  omass  8515  omeu  8520  oen0  8522  oewordi  8527  oewordri  8528  nnarcl  8552  nnmass  8560  brinxper  8673  findcard2  9099  rex2dom  9163  dif1ennnALT  9187  unblem1  9202  unblem2  9203  domunfican  9232  marypha1lem  9346  supiso  9389  inf3lem3  9551  epfrs  9652  frr3g  9680  karden  9819  infxpenlem  9935  iunfictbso  10036  dfac5  10051  dfac2b  10053  kmlem1  10073  kmlem9  10081  infpssrlem3  10227  fin23lem25  10246  fin23lem30  10264  domtriomlem  10364  axdc3lem4  10375  axcclem  10379  zorn2lem7  10424  konigthlem  10491  wunr1om  10642  tskr1om  10690  gruen  10735  grur1a  10742  indpi  10830  genpnmax  10930  prlem934  10956  ltaddpr  10957  ltexprlem7  10965  ltaprlem  10967  axrrecex  11086  axpre-sup  11092  lelttr  11236  dedekind  11309  addlid  11329  nn0lt2  12592  fzind  12627  fnn0ind  12628  btwnz  12632  uzwo  12861  lbzbi  12886  rpnnen1lem5  12931  ledivge1le  13015  xrlelttr  13107  qbtwnre  13151  xrsupsslem  13259  xrinfmsslem  13260  supxrun  13268  elfz1b  13547  elfz0ubfz0  13586  elfzo0z  13656  fzofzim  13664  elfznelfzo  13728  fleqceilz  13813  fsequb  13937  leexp2r  14136  bernneq  14191  fi1uzind  14469  brfi1indALT  14472  swrdnd0  14620  swrdswrdlem  14666  swrdswrd  14667  wrd2ind  14685  swrdccatin1  14687  swrdccatin2  14691  pfxccatin12lem3  14694  repswswrd  14746  cshweqrep  14783  swrd2lsw  14914  2swrd2eqwrdeq  14915  wrdl3s3  14924  s3iunsndisj  14930  cau3lem  15317  climuni  15514  mulcn2  15558  dvdsabseq  16282  divalglem8  16369  ndvdssub  16378  rplpwr  16527  algcvgblem  16546  lcmf  16602  lcmftp  16605  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  lcmfdvdsb  16612  lcmfun  16614  euclemma  16683  prmlem1a  17077  setsstruct2  17144  iscatd  17639  initoeu1  17978  initoeu2  17983  termoeu1  17985  plelttr  18308  insubm  18786  grpinveu  18950  cyccom  19178  symgfixelsi  19410  efgred  19723  telgsumfzs  19964  srgmulgass  20198  srgbinom  20212  lspdisjb  21124  mplcoe5lem  22017  cply1mul  22261  coe1fzgsumd  22269  gsummoncoe1  22273  evl1gsumd  22322  cpmatacl  22681  cpmatmcllem  22683  basis2  22916  0ntr  23036  uncmp  23368  1stcrest  23418  txcls  23569  txcnp  23585  tx1stc  23615  fgss2  23839  alexsubALTlem2  24013  alexsubALTlem3  24014  alexsubALTlem4  24015  metcnp3  24505  tngngp3  24621  reconn  24794  iscau4  25246  ellimc3  25846  ulmbdd  26363  ulmcn  26364  sinq12ge0  26472  gausslemma2dlem3  27331  2sq2  27396  2sqreultlem  27410  2sqreunnltlem  27413  sltsleft  27852  sltsright  27853  noseqind  28284  oldfib  28369  expsgt0  28429  bdayfinbndlem1  28459  bdayfin  28479  elreno2  28487  ax5seglem5  29002  ax5seg  29007  uhgrnbgr0nb  29423  cplgrop  29506  wlkl1loop  29706  uspgr2wlkeq  29714  upgrwlkdvdelem  29804  uhgrwkspthlem2  29822  pthdlem2lem  29835  uspgrn2crct  29876  wlkiswwlks2lem3  29939  wlkiswwlks2  29943  wlkiswwlksupgr2  29945  wlklnwwlkln2lem  29950  wwlksnext  29961  wwlksnextfun  29966  rusgrnumwwlk  30046  clwlkclwwlklem2a4  30067  clwlkclwwlklem3  30071  erclwwlksym  30091  erclwwlknsym  30140  eleclclwwlkn  30146  clwwlknonwwlknonb  30176  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  conngrv2edg  30265  eupth2lem3lem6  30303  frgrncvvdeqlem8  30376  frgrwopreglem4a  30380  frgrreggt1  30463  frgrreg  30464  grpoinveu  30590  ococss  31364  shmodsi  31460  h1datomi  31652  hoaddsub  31887  adjmul  32163  chjatom  32428  atomli  32453  atcvat4i  32468  mdsymlem3  32476  mdsymlem5  32478  mdsymlem6  32479  sumdmdlem  32489  cdj3lem2a  32507  cdj3lem3a  32510  bnj1204  35154  fineqvinfep  35269  umgr2cycllem  35322  umgr2cycl  35323  cvmsdisj  35452  satfv0fun  35553  satffunlem  35583  satffunlem1lem2  35585  satffunlem2lem2  35588  fundmpss  35949  dfon2lem6  35968  dfon2lem8  35970  ifscgr  36226  lineext  36258  fscgr  36262  idinside  36266  btwnconn1lem11  36279  btwnconn1lem12  36280  btwnconn3  36285  brsegle  36290  seglecgr12  36293  hilbert1.2  36337  exp5d  36484  exp5k  36486  nn0prpwlem  36504  mh-inf3f1  36723  bj-restb  37406  exrecfnlem  37695  poimirlem26  37967  poimirlem29  37970  poimirlem32  37973  areacirc  38034  heibor1lem  38130  pridl  38358  pridlc  38392  dmnnzd  38396  disjlem17  39223  membpartlem19  39235  prtlem11  39312  prtlem17  39322  ax12indn  39389  atcvrj0  39874  cvrat4  39889  athgt  39902  lplnexllnN  40010  2llnjN  40013  lvolnle3at  40028  lncmp  40229  paddclN  40288  pexmidlem4N  40419  cdleme17d3  40942  cdleme50trn2  40997  cdlemf2  41008  cdlemf  41009  cdlemj3  41269  cdlemk26b-3  41351  dihord5b  41705  isnacs3  43142  jm2.26  43430  ordnexbtwnsuc  43695  omabs2  43760  naddgeoa  43822  sbiota1  44861  exbir  44906  tratrb  44963  onfrALT  44976  in2an  45035  pwtrrVD  45251  suctrALT2VD  45262  suctrALT2  45263  tratrbVD  45287  trintALTVD  45306  trintALT  45307  or2expropbi  47482  fcoresf1  47517  2reu8i  47561  2reuimp  47563  zm1nn  47750  2ffzoeq  47776  iccpartiltu  47882  iccpartigtl  47883  iccpartgt  47887  iccpartnel  47898  sbcpr  47981  fmtnofac2lem  48031  fmtnofac2  48032  lighneallem2  48069  odd2prm2  48194  stgoldbwt  48252  sbgoldbst  48254  sbgoldbaltlem1  48255  mogoldbb  48261  uhgrimisgrgric  48407  clnbgrgrim  48410  grimedg  48411  gpgedgvtx1  48538  gpgedg2iv  48543  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  pgnbgreunbgr  48601  lidldomn1  48707  ply1mulgsumlem1  48862  lincsumcl  48907  ellcoellss  48911  islinindfis  48925  lindslinindsimp1  48933  lindslinindsimp2lem5  48938  lindsrng01  48944  elfzolborelfzop1  48995  rrx2linest  49218  aacllem  50276