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  3177  mob2  3673  reuind  3711  reupick3  4282  elpwunsn  4641  disjiun  5086  sotr2  5566  wefrc  5618  relop  5799  predpoirr  6291  predfrirr  6292  fnun  6606  mpteqb  6960  tpres  7147  fconst5  7152  funfvima  7176  riotaeqimp  7341  dfwe2  7719  limuni3  7794  tfisi  7801  trom  7817  funcnvuni  7874  resf1ext2b  7877  f1oweALT  7916  frxp  8068  poxp  8070  poxp2  8085  poxp3  8092  wfr3g  8261  onfununi  8273  tz7.48lem  8372  oecl  8464  oaordex  8485  oaass  8488  omwordri  8499  odi  8506  omass  8507  omeu  8512  oen0  8514  oewordi  8519  oewordri  8520  nnarcl  8544  nnmass  8552  brinxper  8664  findcard2  9089  rex2dom  9153  dif1ennnALT  9177  unblem1  9192  unblem2  9193  domunfican  9222  marypha1lem  9336  supiso  9379  inf3lem3  9539  epfrs  9640  frr3g  9668  karden  9807  infxpenlem  9923  iunfictbso  10024  dfac5  10039  dfac2b  10041  kmlem1  10061  kmlem9  10069  infpssrlem3  10215  fin23lem25  10234  fin23lem30  10252  domtriomlem  10352  axdc3lem4  10363  axcclem  10367  zorn2lem7  10412  konigthlem  10479  wunr1om  10630  tskr1om  10678  gruen  10723  grur1a  10730  indpi  10818  genpnmax  10918  prlem934  10944  ltaddpr  10945  ltexprlem7  10953  ltaprlem  10955  axrrecex  11074  axpre-sup  11080  lelttr  11223  dedekind  11296  addlid  11316  nn0lt2  12555  fzind  12590  fnn0ind  12591  btwnz  12595  uzwo  12824  lbzbi  12849  rpnnen1lem5  12894  ledivge1le  12978  xrlelttr  13070  qbtwnre  13114  xrsupsslem  13222  xrinfmsslem  13223  supxrun  13231  elfz1b  13509  elfz0ubfz0  13548  elfzo0z  13617  fzofzim  13625  elfznelfzo  13689  fleqceilz  13774  fsequb  13898  leexp2r  14097  bernneq  14152  fi1uzind  14430  brfi1indALT  14433  swrdnd0  14581  swrdswrdlem  14627  swrdswrd  14628  wrd2ind  14646  swrdccatin1  14648  swrdccatin2  14652  pfxccatin12lem3  14655  repswswrd  14707  cshweqrep  14744  swrd2lsw  14875  2swrd2eqwrdeq  14876  wrdl3s3  14885  s3iunsndisj  14891  cau3lem  15278  climuni  15475  mulcn2  15519  dvdsabseq  16240  divalglem8  16327  ndvdssub  16336  rplpwr  16485  algcvgblem  16504  lcmf  16560  lcmftp  16563  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  lcmfdvdsb  16570  lcmfun  16572  euclemma  16640  prmlem1a  17034  setsstruct2  17101  iscatd  17596  initoeu1  17935  initoeu2  17940  termoeu1  17942  plelttr  18265  insubm  18743  grpinveu  18904  cyccom  19132  symgfixelsi  19364  efgred  19677  telgsumfzs  19918  srgmulgass  20152  srgbinom  20166  lspdisjb  21081  mplcoe5lem  21994  cply1mul  22240  coe1fzgsumd  22248  gsummoncoe1  22252  evl1gsumd  22301  cpmatacl  22660  cpmatmcllem  22662  basis2  22895  0ntr  23015  uncmp  23347  1stcrest  23397  txcls  23548  txcnp  23564  tx1stc  23594  fgss2  23818  alexsubALTlem2  23992  alexsubALTlem3  23993  alexsubALTlem4  23994  metcnp3  24484  tngngp3  24600  reconn  24773  iscau4  25235  ellimc3  25836  ulmbdd  26363  ulmcn  26364  sinq12ge0  26473  gausslemma2dlem3  27335  2sq2  27400  2sqreultlem  27414  2sqreunnltlem  27417  sltsleft  27856  sltsright  27857  noseqind  28288  oldfib  28373  expsgt0  28433  bdayfinbndlem1  28463  bdayfin  28483  elreno2  28491  ax5seglem5  29006  ax5seg  29011  uhgrnbgr0nb  29427  cplgrop  29510  wlkl1loop  29711  uspgr2wlkeq  29719  upgrwlkdvdelem  29809  uhgrwkspthlem2  29827  pthdlem2lem  29840  uspgrn2crct  29881  wlkiswwlks2lem3  29944  wlkiswwlks2  29948  wlkiswwlksupgr2  29950  wlklnwwlkln2lem  29955  wwlksnext  29966  wwlksnextfun  29971  rusgrnumwwlk  30051  clwlkclwwlklem2a4  30072  clwlkclwwlklem3  30076  erclwwlksym  30096  erclwwlknsym  30145  eleclclwwlkn  30151  clwwlknonwwlknonb  30181  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  conngrv2edg  30270  eupth2lem3lem6  30308  frgrncvvdeqlem8  30381  frgrwopreglem4a  30385  frgrreggt1  30468  frgrreg  30469  grpoinveu  30594  ococss  31368  shmodsi  31464  h1datomi  31656  hoaddsub  31891  adjmul  32167  chjatom  32432  atomli  32457  atcvat4i  32472  mdsymlem3  32480  mdsymlem5  32482  mdsymlem6  32483  sumdmdlem  32493  cdj3lem2a  32511  cdj3lem3a  32514  bnj1204  35168  fineqvinfep  35281  umgr2cycllem  35334  umgr2cycl  35335  cvmsdisj  35464  satfv0fun  35565  satffunlem  35595  satffunlem1lem2  35597  satffunlem2lem2  35600  fundmpss  35961  dfon2lem6  35980  dfon2lem8  35982  ifscgr  36238  lineext  36270  fscgr  36274  idinside  36278  btwnconn1lem11  36291  btwnconn1lem12  36292  btwnconn3  36297  brsegle  36302  seglecgr12  36305  hilbert1.2  36349  exp5d  36496  exp5k  36498  nn0prpwlem  36516  bj-restb  37295  exrecfnlem  37580  poimirlem26  37843  poimirlem29  37846  poimirlem32  37849  areacirc  37910  heibor1lem  38006  pridl  38234  pridlc  38268  dmnnzd  38272  disjlem17  39054  membpartlem19  39066  prtlem11  39122  prtlem17  39132  ax12indn  39199  atcvrj0  39684  cvrat4  39699  athgt  39712  lplnexllnN  39820  2llnjN  39823  lvolnle3at  39838  lncmp  40039  paddclN  40098  pexmidlem4N  40229  cdleme17d3  40752  cdleme50trn2  40807  cdlemf2  40818  cdlemf  40819  cdlemj3  41079  cdlemk26b-3  41161  dihord5b  41515  isnacs3  42948  jm2.26  43240  ordnexbtwnsuc  43505  omabs2  43570  naddgeoa  43632  sbiota1  44671  exbir  44716  tratrb  44773  onfrALT  44786  in2an  44845  pwtrrVD  45061  suctrALT2VD  45072  suctrALT2  45073  tratrbVD  45097  trintALTVD  45116  trintALT  45117  or2expropbi  47276  fcoresf1  47311  2reu8i  47355  2reuimp  47357  zm1nn  47544  2ffzoeq  47569  iccpartiltu  47664  iccpartigtl  47665  iccpartgt  47669  iccpartnel  47680  sbcpr  47763  fmtnofac2lem  47810  fmtnofac2  47811  lighneallem2  47848  odd2prm2  47960  stgoldbwt  48018  sbgoldbst  48020  sbgoldbaltlem1  48021  mogoldbb  48027  uhgrimisgrgric  48173  clnbgrgrim  48176  grimedg  48177  gpgedgvtx1  48304  gpgedg2iv  48309  pgnbgreunbgrlem3  48360  pgnbgreunbgrlem6  48366  pgnbgreunbgr  48367  lidldomn1  48473  ply1mulgsumlem1  48628  lincsumcl  48673  ellcoellss  48677  islinindfis  48691  lindslinindsimp1  48699  lindslinindsimp2lem5  48704  lindsrng01  48710  elfzolborelfzop1  48761  rrx2linest  48984  aacllem  50042