Theorem exp31 423

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp31.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
exp31	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem exp31

Step	Hyp	Ref	Expression
1		exp31.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
2	1	ex 416	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	ex 416	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  exp41  438  exp42  439  imp5a  444  expl  461  anasss  470  an31s  664  exbiri  820  3exp  1131  exp516  1369  rexlimdva2  3164  r19.29af2  3269  reusv2lem2  5353  pwssun  5535  onmindif  6434  mpteqb  6989  dffo3f  7081  fompt  7093  fliftfun  7290  elovmpt3rab1  7650  ordsucss  7792  tfindsg  7835  tfrlem1  8339  tfrlem9  8349  oaordi  8508  oaordex  8520  oaass  8523  oarec  8524  omass  8542  oen0  8549  oeordsuc  8557  nnaordi  8581  omsmolem  8620  naddssim  8649  brinxper  8701  infensuc  9120  suppeqfsuppbi  9318  marypha1lem  9372  hartogs  9485  card2on  9495  tz9.12lem3  9740  infxpenlem  9962  cfcoflem  10222  isf32lem12  10314  zorn2lem6  10451  ondomon  10513  axrepnd  10545  fpwwe2lem11  10592  genpcd  10957  ltexprlem6  10992  axpre-sup  11120  negf1o  11610  recex  11812  uzaddcl  12898  nn01to3  12935  rpnnen1lem5  12975  xrsupsslem  13303  xrinfmsslem  13304  supxrunb1  13315  supxrunb2  13316  fz0fzelfz0  13632  fz0fzdiffz0  13635  elfzmlbp  13637  difelfzle  13639  fzo1fzo0n0  13714  elincfzoext  13722  ssfzo12bi  13760  elfznelfzo  13772  modaddmodup  13940  modfzo0difsn  13949  fsuppmapnn0fiubex  13998  seqf1o  14049  expcllem  14078  expeq0  14098  mulexp  14107  hashgt12el2  14429  hashimarni  14447  hash2prd  14481  fi1uzind  14513  swrdnd  14661  swrdswrdlem  14710  swrdswrd  14711  pfxccat3  14740  reuccatpfxs1  14753  repswswrd  14790  repswccat  14792  cshwidxmod  14809  2cshwcshw  14831  s4f1o  14924  wwlktovfo  14964  relexpindlem  15069  resqrex  15267  summo  15734  fsum2d  15788  modfsummods  15811  binom  15850  clim2prod  15908  fprod2d  16001  binomfallfac  16061  efexp  16123  demoivreALT  16223  divconjdvds  16339  addmodlteqALT  16349  dfgcd2  16570  lcmfunsnlem2lem1  16662  lcmfdvdsb  16667  lcmfun  16669  coprmprod  16685  coprmproddvdslem  16686  oddprmdvds  16929  ramcl  17055  prmgaplem6  17082  cshwsidrepswmod0  17120  cshwshashlem1  17121  cshwshashlem2  17122  ressress  17273  initoeu2lem1  18037  symggen  19500  pmtr3ncom  19505  gsumle  20175  srgmulgass  20253  srgbinom  20267  ringinvnzdiv  20337  rhmsubcrngclem2  20703  lmodvsmmulgdi  20951  nzerooringczr  21519  ofldchr  21615  psgndiflemB  21639  assamulgscmlem2  21939  mptcoe1fsupp  22264  coe1fzgsumdlem  22353  evl1gsumdlem  22406  scmatmulcl  22565  mdetdiagid  22647  pm2mpf1  22846  mptcoe1matfsupp  22849  mp2pm2mplem4  22856  chpdmat  22888  chfacfisf  22901  chfacfisfcpmat  22902  chcoeffeq  22933  topbas  23019  elcls  23120  elcls3  23130  2ndcdisj  23503  filufint  23967  ovoliunlem3  25553  dvge0  26055  ulmcn  26449  gausslemma2dlem3  27419  nosupbnd1  27765  nosupbnd2  27767  noinfbnd1  27780  noinfbnd2  27782  sizusglecusg  29620  upgriswlk  29797  2pthnloop  29887  crctcshwlkn0  29977  wlknwwlksnbij  30044  wwlksnred  30048  wwlksnext  30049  wwlksnextinj  30055  wwlksnextproplem2  30066  wwlksnextproplem3  30067  usgr2wspthons3  30123  clwwlkccatlem  30147  clwlkclwwlklem2a4  30155  clwlkclwwlklem2a  30156  clwlkclwwlklem2  30158  erclwwlktr  30180  clwwlkinwwlk  30198  clwwlkf  30205  clwwlkf1  30207  wwlksext2clwwlk  30215  clwwlknscsh  30220  umgr2cwwk2dif  30222  erclwwlkntr  30229  clwwlknonex2  30267  uhgr3cyclex  30340  upgr4cycl4dv4e  30343  eucrctshift  30401  3cyclfrgrrn1  30443  frgrwopreglem2  30471  frgrwopreglem5  30479  frgrwopreglem5ALT  30480  numclwwlk1lem2fo  30516  numclwlk2lem2f  30535  numclwlk2lem2f1o  30537  frgrreg  30552  friendshipgt3  30556  friendship  30557  ipasslem1  30990  shmodsi  31548  elspansn5  31733  h1datomi  31740  nmopsetretALT  32022  pjss2coi  32323  pj3cor1i  32368  mdexchi  32494  atcvat4i  32556  mdsymlem3  32564  mdsymlem4  32565  sumdmdii  32574  cdj3lem2b  32596  elabreximd  32668  iuninc  32719  iundisjf  32748  xrsmulgzz  33147  gsumvsca1  33366  gsumvsca2  33367  unitprodclb  33535  rprmdvdsprod  33690  1arithidom  33693  constrmon  34001  locfinreflem  34097  xrge0iifiso  34192  lmxrge0  34209  esumfzf  34326  sigaclfu2  34378  signstfvneq0  34826  satfrel  35677  satfrnmapom  35680  fmlafvel  35695  fmlasuc  35696  bccolsum  36049  faclimlem1  36053  segletr  36424  segleantisym  36425  outsideoftr  36439  exp5d  36622  elicc3  36637  finxpreclem2  37844  wl-sbcom2d  38024  poimirlem26  38105  mblfinlem3  38118  itg2addnc  38133  indexa  38192  disjlem19  39363  ax12indalem  39529  ax12inda2ALT  39530  cvrat4  40027  elpaddn0  40384  paddasslem5  40408  paddasslem14  40417  eldioph2  43303  pell1234qrdich  43398  oaabsb  43831  onmcl  43868  tfsconcat0b  43883  oaun3lem1  43911  oaun3lem2  43912  naddgeoa  43931  gneispb  44667  rexlimd3  45682  rexabslelem  45952  climsuselem1  46143  stoweidlem19  46553  stoweidlem20  46554  stoweidlem34  46568  wallispilem3  46601  sge0iunmpt  46952  meaiuninc3v  47018  smflimmpt  47344  or2expropbilem1  47586  fsetprcnexALT  47616  2reu8i  47667  2elfz2melfz  47872  subsubelfzo0  47881  iccpartigtl  47989  iccpartgt  47993  icceuelpartlem  48001  fargshiftf1  48007  ich2exprop  48037  ichreuopeq  48039  lighneallem3  48176  gbowgt5  48344  bgoldbtbndlem3  48389  bgoldbtbndlem4  48390  bgoldbtbnd  48391  tgblthelfgott  48397  grimco  48471  isuspgrimlem  48477  grimedg  48517  upgrwlkupwlk  48722  2zrngagrp  48831  lmodvsmdi  48961  ply1mulgsumlem1  48968  elfzolborelfzop1  49101  nnolog2flm1  49172  nn0sumshdiglemA  49201  eenglngeehlnmlem2  49320