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  1115  exp5o  1354  ralrimivv  3197  mob2  3723  reuind  3761  reupick3  4335  elpwunsn  4688  disjiun  5135  sotr2  5629  wefrc  5682  relop  5863  predpoirr  6355  predfrirr  6356  fnun  6682  mpteqb  7034  tpres  7220  fconst5  7225  funfvima  7249  riotaeqimp  7413  dfwe2  7792  limuni3  7872  tfisi  7879  trom  7895  funcnvuni  7954  f1oweALT  7995  frxp  8149  poxp  8151  poxp2  8166  poxp3  8173  wfr3g  8345  wfrlem12OLD  8358  onfununi  8379  tz7.48lem  8479  oecl  8573  oaordex  8594  oaass  8597  omwordri  8608  odi  8615  omass  8616  omeu  8621  oen0  8622  oewordi  8627  oewordri  8628  nnarcl  8652  nnmass  8660  brinxper  8772  findcard2  9202  rex2dom  9279  dif1ennnALT  9308  unblem1  9325  unblem2  9326  domunfican  9358  marypha1lem  9470  supiso  9512  inf3lem3  9667  epfrs  9768  frr3g  9793  karden  9932  infxpenlem  10050  iunfictbso  10151  dfac5  10166  dfac2b  10168  kmlem1  10188  kmlem9  10196  infpssrlem3  10342  fin23lem25  10361  fin23lem30  10379  domtriomlem  10479  axdc3lem4  10490  axcclem  10494  zorn2lem7  10539  konigthlem  10605  wunr1om  10756  tskr1om  10804  gruen  10849  grur1a  10856  indpi  10944  genpnmax  11044  prlem934  11070  ltaddpr  11071  ltexprlem7  11079  ltaprlem  11081  axrrecex  11200  axpre-sup  11206  lelttr  11348  dedekind  11421  addlid  11441  nn0lt2  12678  fzind  12713  fnn0ind  12714  btwnz  12718  uzwo  12950  lbzbi  12975  rpnnen1lem5  13020  ledivge1le  13103  xrlelttr  13194  qbtwnre  13237  xrsupsslem  13345  xrinfmsslem  13346  supxrun  13354  elfz1b  13629  elfz0ubfz0  13668  elfzo0z  13737  fzofzim  13745  elfznelfzo  13807  fleqceilz  13890  fsequb  14012  leexp2r  14210  bernneq  14264  fi1uzind  14542  brfi1indALT  14545  swrdnd0  14691  swrdswrdlem  14738  swrdswrd  14739  wrd2ind  14757  swrdccatin1  14759  swrdccatin2  14763  pfxccatin12lem3  14766  repswswrd  14818  cshweqrep  14855  swrd2lsw  14987  2swrd2eqwrdeq  14988  wrdl3s3  14997  s3iunsndisj  15003  cau3lem  15389  climuni  15584  mulcn2  15628  dvdsabseq  16346  divalglem8  16433  ndvdssub  16442  rplpwr  16591  algcvgblem  16610  lcmf  16666  lcmftp  16669  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  lcmfdvdsb  16676  lcmfun  16678  euclemma  16746  prmlem1a  17140  setsstruct2  17207  iscatd  17717  initoeu1  18064  initoeu2  18069  termoeu1  18071  plelttr  18401  insubm  18843  grpinveu  19004  cyccom  19233  symgfixelsi  19467  efgred  19780  telgsumfzs  20021  srgmulgass  20234  srgbinom  20248  lspdisjb  21145  mplcoe5lem  22074  cply1mul  22315  coe1fzgsumd  22323  gsummoncoe1  22327  evl1gsumd  22376  cpmatacl  22737  cpmatmcllem  22739  basis2  22973  0ntr  23094  uncmp  23426  1stcrest  23476  txcls  23627  txcnp  23643  tx1stc  23673  fgss2  23897  alexsubALTlem2  24071  alexsubALTlem3  24072  alexsubALTlem4  24073  metcnp3  24568  tngngp3  24692  reconn  24863  iscau4  25326  ellimc3  25928  ulmbdd  26455  ulmcn  26456  sinq12ge0  26564  gausslemma2dlem3  27426  2sq2  27491  2sqreultlem  27505  2sqreunnltlem  27508  ssltleft  27923  ssltright  27924  noseqind  28312  expsgt0  28429  ax5seglem5  28962  ax5seg  28967  uhgrnbgr0nb  29385  cplgrop  29468  wlkl1loop  29670  uspgr2wlkeq  29678  upgrwlkdvdelem  29768  uhgrwkspthlem2  29786  pthdlem2lem  29799  uspgrn2crct  29837  wlkiswwlks2lem3  29900  wlkiswwlks2  29904  wlkiswwlksupgr2  29906  wlklnwwlkln2lem  29911  wwlksnext  29922  wwlksnextfun  29927  rusgrnumwwlk  30004  clwlkclwwlklem2a4  30025  clwlkclwwlklem3  30029  erclwwlksym  30049  erclwwlknsym  30098  eleclclwwlkn  30104  clwwlknonwwlknonb  30134  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  conngrv2edg  30223  eupth2lem3lem6  30261  frgrncvvdeqlem8  30334  frgrwopreglem4a  30338  frgrreggt1  30421  frgrreg  30422  grpoinveu  30547  ococss  31321  shmodsi  31417  h1datomi  31609  hoaddsub  31844  adjmul  32120  chjatom  32385  atomli  32410  atcvat4i  32425  mdsymlem3  32433  mdsymlem5  32435  mdsymlem6  32436  sumdmdlem  32446  cdj3lem2a  32464  cdj3lem3a  32467  bnj1204  35004  umgr2cycllem  35124  umgr2cycl  35125  cvmsdisj  35254  satfv0fun  35355  satffunlem  35385  satffunlem1lem2  35387  satffunlem2lem2  35390  fundmpss  35747  dfon2lem6  35769  dfon2lem8  35771  ifscgr  36025  lineext  36057  fscgr  36061  idinside  36065  btwnconn1lem11  36078  btwnconn1lem12  36079  btwnconn3  36084  brsegle  36089  seglecgr12  36092  hilbert1.2  36136  exp5d  36284  exp5k  36286  nn0prpwlem  36304  bj-restb  37076  exrecfnlem  37361  poimirlem26  37632  poimirlem29  37635  poimirlem32  37638  areacirc  37699  heibor1lem  37795  pridl  38023  pridlc  38057  dmnnzd  38061  disjlem17  38780  membpartlem19  38792  prtlem11  38847  prtlem17  38857  ax12indn  38924  atcvrj0  39410  cvrat4  39425  athgt  39438  lplnexllnN  39546  2llnjN  39549  lvolnle3at  39564  lncmp  39765  paddclN  39824  pexmidlem4N  39955  cdleme17d3  40478  cdleme50trn2  40533  cdlemf2  40544  cdlemf  40545  cdlemj3  40805  cdlemk26b-3  40887  dihord5b  41241  isnacs3  42697  jm2.26  42990  ordnexbtwnsuc  43256  omabs2  43321  naddgeoa  43383  sbiota1  44429  exbir  44475  tratrb  44533  onfrALT  44546  in2an  44605  pwtrrVD  44822  suctrALT2VD  44833  suctrALT2  44834  tratrbVD  44858  trintALTVD  44877  trintALT  44878  or2expropbi  46983  fcoresf1  47018  2reu8i  47062  2reuimp  47064  zm1nn  47251  2ffzoeq  47276  iccpartiltu  47346  iccpartigtl  47347  iccpartgt  47351  iccpartnel  47362  sbcpr  47445  fmtnofac2lem  47492  fmtnofac2  47493  lighneallem2  47530  odd2prm2  47642  stgoldbwt  47700  sbgoldbst  47702  sbgoldbaltlem1  47703  mogoldbb  47709  uhgrimisgrgric  47836  clnbgrgrim  47839  grimedg  47840  gpgedgvtx1  47954  lidldomn1  48074  ply1mulgsumlem1  48231  lincsumcl  48276  ellcoellss  48280  islinindfis  48294  lindslinindsimp1  48302  lindslinindsimp2lem5  48307  lindsrng01  48313  elfzolborelfzop1  48364  rrx2linest  48591  aacllem  49031