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  3171  mob2  3672  reuind  3710  reupick3  4278  elpwunsn  4635  disjiun  5077  sotr2  5556  wefrc  5608  relop  5788  predpoirr  6276  predfrirr  6277  fnun  6591  mpteqb  6943  tpres  7130  fconst5  7135  funfvima  7159  riotaeqimp  7324  dfwe2  7702  limuni3  7777  tfisi  7784  trom  7800  funcnvuni  7857  resf1ext2b  7860  f1oweALT  7899  frxp  8051  poxp  8053  poxp2  8068  poxp3  8075  wfr3g  8244  onfununi  8256  tz7.48lem  8355  oecl  8447  oaordex  8468  oaass  8471  omwordri  8482  odi  8489  omass  8490  omeu  8495  oen0  8496  oewordi  8501  oewordri  8502  nnarcl  8526  nnmass  8534  brinxper  8646  findcard2  9069  rex2dom  9132  dif1ennnALT  9156  unblem1  9171  unblem2  9172  domunfican  9201  marypha1lem  9312  supiso  9355  inf3lem3  9515  epfrs  9616  frr3g  9641  karden  9780  infxpenlem  9896  iunfictbso  9997  dfac5  10012  dfac2b  10014  kmlem1  10034  kmlem9  10042  infpssrlem3  10188  fin23lem25  10207  fin23lem30  10225  domtriomlem  10325  axdc3lem4  10336  axcclem  10340  zorn2lem7  10385  konigthlem  10451  wunr1om  10602  tskr1om  10650  gruen  10695  grur1a  10702  indpi  10790  genpnmax  10890  prlem934  10916  ltaddpr  10917  ltexprlem7  10925  ltaprlem  10927  axrrecex  11046  axpre-sup  11052  lelttr  11195  dedekind  11268  addlid  11288  nn0lt2  12528  fzind  12563  fnn0ind  12564  btwnz  12568  uzwo  12801  lbzbi  12826  rpnnen1lem5  12871  ledivge1le  12955  xrlelttr  13047  qbtwnre  13090  xrsupsslem  13198  xrinfmsslem  13199  supxrun  13207  elfz1b  13485  elfz0ubfz0  13524  elfzo0z  13593  fzofzim  13601  elfznelfzo  13665  fleqceilz  13750  fsequb  13874  leexp2r  14073  bernneq  14128  fi1uzind  14406  brfi1indALT  14409  swrdnd0  14557  swrdswrdlem  14603  swrdswrd  14604  wrd2ind  14622  swrdccatin1  14624  swrdccatin2  14628  pfxccatin12lem3  14631  repswswrd  14683  cshweqrep  14720  swrd2lsw  14851  2swrd2eqwrdeq  14852  wrdl3s3  14861  s3iunsndisj  14867  cau3lem  15254  climuni  15451  mulcn2  15495  dvdsabseq  16216  divalglem8  16303  ndvdssub  16312  rplpwr  16461  algcvgblem  16480  lcmf  16536  lcmftp  16539  lcmfunsnlem2lem1  16541  lcmfunsnlem2lem2  16542  lcmfdvdsb  16546  lcmfun  16548  euclemma  16616  prmlem1a  17010  setsstruct2  17077  iscatd  17571  initoeu1  17910  initoeu2  17915  termoeu1  17917  plelttr  18240  insubm  18718  grpinveu  18879  cyccom  19108  symgfixelsi  19340  efgred  19653  telgsumfzs  19894  srgmulgass  20128  srgbinom  20142  lspdisjb  21056  mplcoe5lem  21967  cply1mul  22204  coe1fzgsumd  22212  gsummoncoe1  22216  evl1gsumd  22265  cpmatacl  22624  cpmatmcllem  22626  basis2  22859  0ntr  22979  uncmp  23311  1stcrest  23361  txcls  23512  txcnp  23528  tx1stc  23558  fgss2  23782  alexsubALTlem2  23956  alexsubALTlem3  23957  alexsubALTlem4  23958  metcnp3  24448  tngngp3  24564  reconn  24737  iscau4  25199  ellimc3  25800  ulmbdd  26327  ulmcn  26328  sinq12ge0  26437  gausslemma2dlem3  27299  2sq2  27364  2sqreultlem  27378  2sqreunnltlem  27381  ssltleft  27808  ssltright  27809  noseqind  28215  expsgt0  28353  ax5seglem5  28904  ax5seg  28909  uhgrnbgr0nb  29325  cplgrop  29408  wlkl1loop  29609  uspgr2wlkeq  29617  upgrwlkdvdelem  29707  uhgrwkspthlem2  29725  pthdlem2lem  29738  uspgrn2crct  29779  wlkiswwlks2lem3  29842  wlkiswwlks2  29846  wlkiswwlksupgr2  29848  wlklnwwlkln2lem  29853  wwlksnext  29864  wwlksnextfun  29869  rusgrnumwwlk  29946  clwlkclwwlklem2a4  29967  clwlkclwwlklem3  29971  erclwwlksym  29991  erclwwlknsym  30040  eleclclwwlkn  30046  clwwlknonwwlknonb  30076  upgr3v3e3cycl  30150  upgr4cycl4dv4e  30155  conngrv2edg  30165  eupth2lem3lem6  30203  frgrncvvdeqlem8  30276  frgrwopreglem4a  30280  frgrreggt1  30363  frgrreg  30364  grpoinveu  30489  ococss  31263  shmodsi  31359  h1datomi  31551  hoaddsub  31786  adjmul  32062  chjatom  32327  atomli  32352  atcvat4i  32367  mdsymlem3  32375  mdsymlem5  32377  mdsymlem6  32378  sumdmdlem  32388  cdj3lem2a  32406  cdj3lem3a  32409  bnj1204  35014  umgr2cycllem  35152  umgr2cycl  35153  cvmsdisj  35282  satfv0fun  35383  satffunlem  35413  satffunlem1lem2  35415  satffunlem2lem2  35418  fundmpss  35779  dfon2lem6  35801  dfon2lem8  35803  ifscgr  36057  lineext  36089  fscgr  36093  idinside  36097  btwnconn1lem11  36110  btwnconn1lem12  36111  btwnconn3  36116  brsegle  36121  seglecgr12  36124  hilbert1.2  36168  exp5d  36315  exp5k  36317  nn0prpwlem  36335  bj-restb  37107  exrecfnlem  37392  poimirlem26  37665  poimirlem29  37668  poimirlem32  37671  areacirc  37732  heibor1lem  37828  pridl  38056  pridlc  38090  dmnnzd  38094  disjlem17  38816  membpartlem19  38828  prtlem11  38884  prtlem17  38894  ax12indn  38961  atcvrj0  39446  cvrat4  39461  athgt  39474  lplnexllnN  39582  2llnjN  39585  lvolnle3at  39600  lncmp  39801  paddclN  39860  pexmidlem4N  39991  cdleme17d3  40514  cdleme50trn2  40569  cdlemf2  40580  cdlemf  40581  cdlemj3  40841  cdlemk26b-3  40923  dihord5b  41277  isnacs3  42722  jm2.26  43014  ordnexbtwnsuc  43279  omabs2  43344  naddgeoa  43406  sbiota1  44446  exbir  44491  tratrb  44548  onfrALT  44561  in2an  44620  pwtrrVD  44836  suctrALT2VD  44847  suctrALT2  44848  tratrbVD  44872  trintALTVD  44891  trintALT  44892  or2expropbi  47044  fcoresf1  47079  2reu8i  47123  2reuimp  47125  zm1nn  47312  2ffzoeq  47337  iccpartiltu  47432  iccpartigtl  47433  iccpartgt  47437  iccpartnel  47448  sbcpr  47531  fmtnofac2lem  47578  fmtnofac2  47579  lighneallem2  47616  odd2prm2  47728  stgoldbwt  47786  sbgoldbst  47788  sbgoldbaltlem1  47789  mogoldbb  47795  uhgrimisgrgric  47941  clnbgrgrim  47944  grimedg  47945  gpgedgvtx1  48072  gpgedg2iv  48077  pgnbgreunbgrlem3  48128  pgnbgreunbgrlem6  48134  pgnbgreunbgr  48135  lidldomn1  48241  ply1mulgsumlem1  48397  lincsumcl  48442  ellcoellss  48446  islinindfis  48460  lindslinindsimp1  48468  lindslinindsimp2lem5  48473  lindsrng01  48479  elfzolborelfzop1  48530  rrx2linest  48753  aacllem  49812