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  602  mpan2d  693  a2and  844  3impib  1116  exp5o  1355  ralrimivv  3206  mob2  3737  reuind  3775  reupick3  4349  elpwunsn  4707  disjiun  5154  sotr2  5641  wefrc  5694  relop  5875  predpoirr  6365  predfrirr  6366  fnun  6693  mpteqb  7048  tpres  7238  fconst5  7243  funfvima  7267  riotaeqimp  7431  dfwe2  7809  limuni3  7889  tfisi  7896  trom  7912  funcnvuni  7972  f1oweALT  8013  frxp  8167  poxp  8169  poxp2  8184  poxp3  8191  wfr3g  8363  wfrlem12OLD  8376  onfununi  8397  tz7.48lem  8497  oecl  8593  oaordex  8614  oaass  8617  omwordri  8628  odi  8635  omass  8636  omeu  8641  oen0  8642  oewordi  8647  oewordri  8648  nnarcl  8672  nnmass  8680  brinxper  8792  findcard2  9230  rex2dom  9309  dif1ennnALT  9339  unblem1  9356  unblem2  9357  domunfican  9389  marypha1lem  9502  supiso  9544  inf3lem3  9699  epfrs  9800  frr3g  9825  karden  9964  infxpenlem  10082  iunfictbso  10183  dfac5  10198  dfac2b  10200  kmlem1  10220  kmlem9  10228  infpssrlem3  10374  fin23lem25  10393  fin23lem30  10411  domtriomlem  10511  axdc3lem4  10522  axcclem  10526  zorn2lem7  10571  konigthlem  10637  wunr1om  10788  tskr1om  10836  gruen  10881  grur1a  10888  indpi  10976  genpnmax  11076  prlem934  11102  ltaddpr  11103  ltexprlem7  11111  ltaprlem  11113  axrrecex  11232  axpre-sup  11238  lelttr  11380  dedekind  11453  addlid  11473  nn0lt2  12706  fzind  12741  fnn0ind  12742  btwnz  12746  uzwo  12976  lbzbi  13001  rpnnen1lem5  13046  ledivge1le  13128  xrlelttr  13218  qbtwnre  13261  xrsupsslem  13369  xrinfmsslem  13370  supxrun  13378  elfz1b  13653  elfz0ubfz0  13689  elfzo0z  13758  fzofzim  13763  elfznelfzo  13822  fleqceilz  13905  fsequb  14026  leexp2r  14224  bernneq  14278  fi1uzind  14556  brfi1indALT  14559  swrdnd0  14705  swrdswrdlem  14752  swrdswrd  14753  wrd2ind  14771  swrdccatin1  14773  swrdccatin2  14777  pfxccatin12lem3  14780  repswswrd  14832  cshweqrep  14869  swrd2lsw  15001  2swrd2eqwrdeq  15002  wrdl3s3  15011  s3iunsndisj  15017  cau3lem  15403  climuni  15598  mulcn2  15642  dvdsabseq  16361  divalglem8  16448  ndvdssub  16457  rplpwr  16605  algcvgblem  16624  lcmf  16680  lcmftp  16683  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  lcmfdvdsb  16690  lcmfun  16692  euclemma  16760  prmlem1a  17154  setsstruct2  17221  iscatd  17731  initoeu1  18078  initoeu2  18083  termoeu1  18085  plelttr  18414  insubm  18853  grpinveu  19014  cyccom  19243  symgfixelsi  19477  efgred  19790  telgsumfzs  20031  srgmulgass  20244  srgbinom  20258  lspdisjb  21151  mplcoe5lem  22080  cply1mul  22321  coe1fzgsumd  22329  gsummoncoe1  22333  evl1gsumd  22382  cpmatacl  22743  cpmatmcllem  22745  basis2  22979  0ntr  23100  uncmp  23432  1stcrest  23482  txcls  23633  txcnp  23649  tx1stc  23679  fgss2  23903  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALTlem4  24079  metcnp3  24574  tngngp3  24698  reconn  24869  iscau4  25332  ellimc3  25934  ulmbdd  26459  ulmcn  26460  sinq12ge0  26568  gausslemma2dlem3  27430  2sq2  27495  2sqreultlem  27509  2sqreunnltlem  27512  ssltleft  27927  ssltright  27928  noseqind  28316  expsgt0  28433  ax5seglem5  28966  ax5seg  28971  uhgrnbgr0nb  29389  cplgrop  29472  wlkl1loop  29674  uspgr2wlkeq  29682  upgrwlkdvdelem  29772  uhgrwkspthlem2  29790  pthdlem2lem  29803  uspgrn2crct  29841  wlkiswwlks2lem3  29904  wlkiswwlks2  29908  wlkiswwlksupgr2  29910  wlklnwwlkln2lem  29915  wwlksnext  29926  wwlksnextfun  29931  rusgrnumwwlk  30008  clwlkclwwlklem2a4  30029  clwlkclwwlklem3  30033  erclwwlksym  30053  erclwwlknsym  30102  eleclclwwlkn  30108  clwwlknonwwlknonb  30138  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  conngrv2edg  30227  eupth2lem3lem6  30265  frgrncvvdeqlem8  30338  frgrwopreglem4a  30342  frgrreggt1  30425  frgrreg  30426  grpoinveu  30551  ococss  31325  shmodsi  31421  h1datomi  31613  hoaddsub  31848  adjmul  32124  chjatom  32389  atomli  32414  atcvat4i  32429  mdsymlem3  32437  mdsymlem5  32439  mdsymlem6  32440  sumdmdlem  32450  cdj3lem2a  32468  cdj3lem3a  32471  bnj1204  34988  umgr2cycllem  35108  umgr2cycl  35109  cvmsdisj  35238  satfv0fun  35339  satffunlem  35369  satffunlem1lem2  35371  satffunlem2lem2  35374  fundmpss  35730  dfon2lem6  35752  dfon2lem8  35754  ifscgr  36008  lineext  36040  fscgr  36044  idinside  36048  btwnconn1lem11  36061  btwnconn1lem12  36062  btwnconn3  36067  brsegle  36072  seglecgr12  36075  hilbert1.2  36119  exp5d  36268  exp5k  36270  nn0prpwlem  36288  bj-restb  37060  exrecfnlem  37345  poimirlem26  37606  poimirlem29  37609  poimirlem32  37612  areacirc  37673  heibor1lem  37769  pridl  37997  pridlc  38031  dmnnzd  38035  disjlem17  38755  membpartlem19  38767  prtlem11  38822  prtlem17  38832  ax12indn  38899  atcvrj0  39385  cvrat4  39400  athgt  39413  lplnexllnN  39521  2llnjN  39524  lvolnle3at  39539  lncmp  39740  paddclN  39799  pexmidlem4N  39930  cdleme17d3  40453  cdleme50trn2  40508  cdlemf2  40519  cdlemf  40520  cdlemj3  40780  cdlemk26b-3  40862  dihord5b  41216  isnacs3  42666  jm2.26  42959  ordnexbtwnsuc  43229  omabs2  43294  naddgeoa  43356  sbiota1  44403  exbir  44449  tratrb  44507  onfrALT  44520  in2an  44579  pwtrrVD  44796  suctrALT2VD  44807  suctrALT2  44808  tratrbVD  44832  trintALTVD  44851  trintALT  44852  or2expropbi  46949  fcoresf1  46984  2reu8i  47028  2reuimp  47030  zm1nn  47217  2ffzoeq  47242  iccpartiltu  47296  iccpartigtl  47297  iccpartgt  47301  iccpartnel  47312  sbcpr  47395  fmtnofac2lem  47442  fmtnofac2  47443  lighneallem2  47480  odd2prm2  47592  stgoldbwt  47650  sbgoldbst  47652  sbgoldbaltlem1  47653  mogoldbb  47659  uhgrimisgrgric  47783  clnbgrgrim  47786  grimedg  47787  lidldomn1  47954  ply1mulgsumlem1  48115  lincsumcl  48160  ellcoellss  48164  islinindfis  48178  lindslinindsimp1  48186  lindslinindsimp2lem5  48191  lindsrng01  48197  elfzolborelfzop1  48248  rrx2linest  48476  aacllem  48895