Theorem expd 416

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 415	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	com3r 87	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  expcomd  417  exp32  421  exp4b  431  exp4c  433  exp4d  434  exp42  436  exp44  438  exp5c  445  exp5j  446  exp5l  447  pm3.3  449  expdimp  453  impl  456  syland  602  mpan2d  690  a2and  840  3impib  1109  exp5o  1348  ralrimivv  3157  mob2  3642  reuind  3678  reupick3  4208  elpwunsn  4528  disjiun  4950  sotr2  5393  wefrc  5437  relop  5607  predpoirr  6051  predfrirr  6052  fnun  6333  mpteqb  6653  tpres  6830  fconst5  6835  funfvima  6858  riotaeqimp  7000  dfwe2  7352  limuni3  7423  tfisi  7429  ordom  7445  funcnvuni  7492  f1oweALT  7529  frxp  7673  poxp  7675  wfr3g  7804  wfrlem12  7818  onfununi  7830  tz7.48lem  7928  oecl  8013  oaordex  8034  oaass  8037  omwordri  8048  odi  8055  omass  8056  omeu  8061  oen0  8062  oewordi  8067  oewordri  8068  nnarcl  8092  nnmass  8100  dif1en  8597  findcard2  8604  unblem1  8616  unblem2  8617  domunfican  8637  marypha1lem  8743  supiso  8785  inf3lem3  8939  epfrs  9019  karden  9170  infxpenlem  9285  iunfictbso  9386  dfac5  9400  dfac2b  9402  kmlem1  9422  kmlem9  9430  infpssrlem3  9573  fin23lem25  9592  fin23lem30  9610  domtriomlem  9710  axdc3lem4  9721  axcclem  9725  zorn2lem7  9770  konigthlem  9836  wunr1om  9987  tskr1om  10035  gruen  10080  grur1a  10087  indpi  10175  genpnmax  10275  prlem934  10301  ltaddpr  10302  ltexprlem7  10310  ltaprlem  10312  axrrecex  10431  axpre-sup  10437  lelttr  10578  dedekind  10650  addid2  10670  nn0lt2  11894  fzind  11929  fnn0ind  11930  btwnz  11933  uzwo  12160  lbzbi  12185  rpnnen1lem5  12230  ledivge1le  12310  xrlelttr  12399  qbtwnre  12442  xrsupsslem  12550  xrinfmsslem  12551  supxrun  12559  elfz1b  12826  elfz0ubfz0  12861  elfzo0z  12929  fzofzim  12934  elfznelfzo  12992  fleqceilz  13072  fsequb  13193  leexp2r  13388  bernneq  13440  fi1uzind  13701  brfi1indALT  13704  swrdnd0  13855  swrdswrdlem  13902  swrdswrd  13903  wrd2ind  13921  swrdccatin1  13923  swrdccatin2  13927  pfxccatin12lem3  13930  repswswrd  13982  cshweqrep  14019  swrd2lsw  14150  2swrd2eqwrdeq  14151  wrdl3s3  14160  s3iunsndisj  14162  cau3lem  14548  climuni  14743  mulcn2  14786  dvdsabseq  15496  divalglem8  15584  ndvdssub  15593  rplpwr  15736  algcvgblem  15750  lcmf  15806  lcmftp  15809  lcmfunsnlem2lem1  15811  lcmfunsnlem2lem2  15812  lcmfdvdsb  15816  lcmfun  15818  euclemma  15886  prmlem1a  16269  setsstruct2  16350  iscatd  16773  initoeu1  17100  initoeu2  17105  termoeu1  17107  plelttr  17411  grpinveu  17895  symgfixelsi  18294  efgred  18601  telgsumfzs  18826  srgmulgass  18971  srgbinom  18985  lspdisjb  19588  mplcoe5lem  19935  cply1mul  20145  coe1fzgsumd  20153  gsummoncoe1  20155  evl1gsumd  20202  cpmatacl  21008  cpmatmcllem  21010  basis2  21243  0ntr  21363  uncmp  21695  1stcrest  21745  txcls  21896  txcnp  21912  tx1stc  21942  fgss2  22166  alexsubALTlem2  22340  alexsubALTlem3  22341  alexsubALTlem4  22342  metcnp3  22833  tngngp3  22948  reconn  23119  iscau4  23565  ellimc3  24160  ulmbdd  24669  ulmcn  24670  sinq12ge0  24777  gausslemma2dlem3  25626  2sq2  25691  2sqreultlem  25705  2sqreunnltlem  25708  ax5seglem5  26402  ax5seg  26407  uhgrnbgr0nb  26819  cplgrop  26902  wlkl1loop  27102  uspgr2wlkeq  27110  wlkresOLD  27137  upgrwlkdvdelem  27204  uhgrwkspthlem2  27222  pthdlem2lem  27235  uspgrn2crct  27273  wlkiswwlks2lem3  27336  wlkiswwlks2  27340  wlkiswwlksupgr2  27342  wlklnwwlkln2lem  27347  wwlksnext  27358  wwlksnextfun  27363  rusgrnumwwlk  27441  clwlkclwwlklem2a4  27462  clwlkclwwlklem3  27466  erclwwlksym  27486  erclwwlknsym  27536  eleclclwwlkn  27542  clwwlknonwwlknonb  27572  upgr3v3e3cycl  27646  upgr4cycl4dv4e  27651  conngrv2edg  27661  eupth2lem3lem6  27700  frgrncvvdeqlem8  27777  frgrwopreglem4a  27781  frgrreggt1  27864  frgrreg  27865  grpoinveu  27987  ococss  28761  shmodsi  28857  h1datomi  29049  hoaddsub  29284  adjmul  29560  chjatom  29825  atomli  29850  atcvat4i  29865  mdsymlem3  29873  mdsymlem5  29875  mdsymlem6  29876  sumdmdlem  29886  cdj3lem2a  29904  cdj3lem3a  29907  bnj1204  31898  umgr2cycllem  31996  umgr2cycl  31997  cvmsdisj  32126  satfv0fun  32227  satffunlem  32257  satffunlem1lem2  32259  satffunlem2lem2  32262  fundmpss  32618  dfon2lem6  32642  dfon2lem8  32644  frr3g  32731  ifscgr  33115  lineext  33147  fscgr  33151  idinside  33155  btwnconn1lem11  33168  btwnconn1lem12  33169  btwnconn3  33174  brsegle  33179  seglecgr12  33182  hilbert1.2  33226  exp5d  33260  exp5k  33262  nn0prpwlem  33280  bj-restb  34003  exrecfnlem  34210  poimirlem26  34468  poimirlem29  34471  poimirlem32  34474  areacirc  34537  heibor1lem  34638  pridl  34866  pridlc  34900  dmnnzd  34904  prtlem11  35552  prtlem17  35562  ax12indn  35629  atcvrj0  36114  cvrat4  36129  athgt  36142  lplnexllnN  36250  2llnjN  36253  lvolnle3at  36268  lncmp  36469  paddclN  36528  pexmidlem4N  36659  cdleme17d3  37182  cdleme50trn2  37237  cdlemf2  37248  cdlemf  37249  cdlemj3  37509  cdlemk26b-3  37591  dihord5b  37945  isnacs3  38811  jm2.26  39103  sbiota1  40323  exbir  40370  tratrb  40428  onfrALT  40441  in2an  40500  pwtrrVD  40717  suctrALT2VD  40728  suctrALT2  40729  tratrbVD  40753  trintALTVD  40772  trintALT  40773  or2expropbi  42805  2reu8i  42848  2reuimp  42850  zm1nn  43038  2ffzoeq  43064  iccpartiltu  43084  iccpartigtl  43085  iccpartgt  43089  iccpartnel  43100  sbcpr  43185  fmtnofac2lem  43232  fmtnofac2  43233  lighneallem2  43273  odd2prm2  43385  stgoldbwt  43443  sbgoldbst  43445  sbgoldbaltlem1  43446  mogoldbb  43452  isomuspgrlem1  43494  isomuspgrlem2d  43498  lidldomn1  43690  ply1mulgsumlem1  43940  lincsumcl  43986  ellcoellss  43990  islinindfis  44004  lindslinindsimp1  44012  lindslinindsimp2lem5  44017  lindsrng01  44023  elfzolborelfzop1  44075  rrx2linest  44230  aacllem  44402