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  1356  ralrimivv  3170  mob2  3677  reuind  3715  reupick3  4283  elpwunsn  4638  disjiun  5083  sotr2  5565  wefrc  5617  relop  5797  predpoirr  6285  predfrirr  6286  fnun  6600  mpteqb  6953  tpres  7141  fconst5  7146  funfvima  7170  riotaeqimp  7336  dfwe2  7714  limuni3  7792  tfisi  7799  trom  7815  funcnvuni  7872  resf1ext2b  7875  f1oweALT  7914  frxp  8066  poxp  8068  poxp2  8083  poxp3  8090  wfr3g  8259  onfununi  8271  tz7.48lem  8370  oecl  8462  oaordex  8483  oaass  8486  omwordri  8497  odi  8504  omass  8505  omeu  8510  oen0  8511  oewordi  8516  oewordri  8517  nnarcl  8541  nnmass  8549  brinxper  8661  findcard2  9088  rex2dom  9152  dif1ennnALT  9180  unblem1  9197  unblem2  9198  domunfican  9230  marypha1lem  9342  supiso  9385  inf3lem3  9545  epfrs  9646  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  10481  wunr1om  10632  tskr1om  10680  gruen  10725  grur1a  10732  indpi  10820  genpnmax  10920  prlem934  10946  ltaddpr  10947  ltexprlem7  10955  ltaprlem  10957  axrrecex  11076  axpre-sup  11082  lelttr  11224  dedekind  11297  addlid  11317  nn0lt2  12557  fzind  12592  fnn0ind  12593  btwnz  12597  uzwo  12830  lbzbi  12855  rpnnen1lem5  12900  ledivge1le  12984  xrlelttr  13076  qbtwnre  13119  xrsupsslem  13227  xrinfmsslem  13228  supxrun  13236  elfz1b  13514  elfz0ubfz0  13553  elfzo0z  13622  fzofzim  13630  elfznelfzo  13693  fleqceilz  13776  fsequb  13900  leexp2r  14099  bernneq  14154  fi1uzind  14432  brfi1indALT  14435  swrdnd0  14582  swrdswrdlem  14628  swrdswrd  14629  wrd2ind  14647  swrdccatin1  14649  swrdccatin2  14653  pfxccatin12lem3  14656  repswswrd  14708  cshweqrep  14745  swrd2lsw  14877  2swrd2eqwrdeq  14878  wrdl3s3  14887  s3iunsndisj  14893  cau3lem  15280  climuni  15477  mulcn2  15521  dvdsabseq  16242  divalglem8  16329  ndvdssub  16338  rplpwr  16487  algcvgblem  16506  lcmf  16562  lcmftp  16565  lcmfunsnlem2lem1  16567  lcmfunsnlem2lem2  16568  lcmfdvdsb  16572  lcmfun  16574  euclemma  16642  prmlem1a  17036  setsstruct2  17103  iscatd  17597  initoeu1  17936  initoeu2  17941  termoeu1  17943  plelttr  18266  insubm  18710  grpinveu  18871  cyccom  19100  symgfixelsi  19332  efgred  19645  telgsumfzs  19886  srgmulgass  20120  srgbinom  20134  lspdisjb  21051  mplcoe5lem  21962  cply1mul  22199  coe1fzgsumd  22207  gsummoncoe1  22211  evl1gsumd  22260  cpmatacl  22619  cpmatmcllem  22621  basis2  22854  0ntr  22974  uncmp  23306  1stcrest  23356  txcls  23507  txcnp  23523  tx1stc  23553  fgss2  23777  alexsubALTlem2  23951  alexsubALTlem3  23952  alexsubALTlem4  23953  metcnp3  24444  tngngp3  24560  reconn  24733  iscau4  25195  ellimc3  25796  ulmbdd  26323  ulmcn  26324  sinq12ge0  26433  gausslemma2dlem3  27295  2sq2  27360  2sqreultlem  27374  2sqreunnltlem  27377  ssltleft  27802  ssltright  27803  noseqind  28209  expsgt0  28347  ax5seglem5  28896  ax5seg  28901  uhgrnbgr0nb  29317  cplgrop  29400  wlkl1loop  29601  uspgr2wlkeq  29609  upgrwlkdvdelem  29699  uhgrwkspthlem2  29717  pthdlem2lem  29730  uspgrn2crct  29771  wlkiswwlks2lem3  29834  wlkiswwlks2  29838  wlkiswwlksupgr2  29840  wlklnwwlkln2lem  29845  wwlksnext  29856  wwlksnextfun  29861  rusgrnumwwlk  29938  clwlkclwwlklem2a4  29959  clwlkclwwlklem3  29963  erclwwlksym  29983  erclwwlknsym  30032  eleclclwwlkn  30038  clwwlknonwwlknonb  30068  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  conngrv2edg  30157  eupth2lem3lem6  30195  frgrncvvdeqlem8  30268  frgrwopreglem4a  30272  frgrreggt1  30355  frgrreg  30356  grpoinveu  30481  ococss  31255  shmodsi  31351  h1datomi  31543  hoaddsub  31778  adjmul  32054  chjatom  32319  atomli  32344  atcvat4i  32359  mdsymlem3  32367  mdsymlem5  32369  mdsymlem6  32370  sumdmdlem  32380  cdj3lem2a  32398  cdj3lem3a  32401  bnj1204  34978  umgr2cycllem  35112  umgr2cycl  35113  cvmsdisj  35242  satfv0fun  35343  satffunlem  35373  satffunlem1lem2  35375  satffunlem2lem2  35378  fundmpss  35739  dfon2lem6  35761  dfon2lem8  35763  ifscgr  36017  lineext  36049  fscgr  36053  idinside  36057  btwnconn1lem11  36070  btwnconn1lem12  36071  btwnconn3  36076  brsegle  36081  seglecgr12  36084  hilbert1.2  36128  exp5d  36275  exp5k  36277  nn0prpwlem  36295  bj-restb  37067  exrecfnlem  37352  poimirlem26  37625  poimirlem29  37628  poimirlem32  37631  areacirc  37692  heibor1lem  37788  pridl  38016  pridlc  38050  dmnnzd  38054  disjlem17  38776  membpartlem19  38788  prtlem11  38844  prtlem17  38854  ax12indn  38921  atcvrj0  39407  cvrat4  39422  athgt  39435  lplnexllnN  39543  2llnjN  39546  lvolnle3at  39561  lncmp  39762  paddclN  39821  pexmidlem4N  39952  cdleme17d3  40475  cdleme50trn2  40530  cdlemf2  40541  cdlemf  40542  cdlemj3  40802  cdlemk26b-3  40884  dihord5b  41238  isnacs3  42683  jm2.26  42975  ordnexbtwnsuc  43240  omabs2  43305  naddgeoa  43367  sbiota1  44407  exbir  44453  tratrb  44510  onfrALT  44523  in2an  44582  pwtrrVD  44798  suctrALT2VD  44809  suctrALT2  44810  tratrbVD  44834  trintALTVD  44853  trintALT  44854  or2expropbi  47019  fcoresf1  47054  2reu8i  47098  2reuimp  47100  zm1nn  47287  2ffzoeq  47312  iccpartiltu  47407  iccpartigtl  47408  iccpartgt  47412  iccpartnel  47423  sbcpr  47506  fmtnofac2lem  47553  fmtnofac2  47554  lighneallem2  47591  odd2prm2  47703  stgoldbwt  47761  sbgoldbst  47763  sbgoldbaltlem1  47764  mogoldbb  47770  uhgrimisgrgric  47915  clnbgrgrim  47918  grimedg  47919  gpgedgvtx1  48037  gpgedg2iv  48042  pgnbgreunbgrlem3  48092  pgnbgreunbgrlem6  48098  pgnbgreunbgr  48099  lidldomn1  48203  ply1mulgsumlem1  48359  lincsumcl  48404  ellcoellss  48408  islinindfis  48422  lindslinindsimp1  48430  lindslinindsimp2lem5  48435  lindsrng01  48441  elfzolborelfzop1  48492  rrx2linest  48715  aacllem  49774