Theorem exp31 419

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 412	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	ex 412	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:  exp41  434  exp42  435  imp5a  440  expl  457  anasss  466  an31s  654  exbiri  811  3exp  1118  exp516  1355  rexlimdva2  3154  r19.29af2  3264  reusv2lem2  5404  pwssun  5579  onmindif  6477  mpteqb  7034  dffo3f  7125  fompt  7137  fliftfun  7331  elovmpt3rab1  7692  ordsucss  7837  tfindsg  7881  tfrlem1  8414  tfrlem9  8423  oaordi  8582  oaordex  8594  oaass  8597  oarec  8598  omass  8616  oen0  8622  oeordsuc  8630  nnaordi  8654  omsmolem  8693  naddssim  8721  brinxper  8772  infensuc  9193  php3OLD  9258  suppeqfsuppbi  9416  marypha1lem  9470  hartogs  9581  card2on  9591  tz9.12lem3  9826  infxpenlem  10050  cfcoflem  10309  isf32lem12  10401  zorn2lem6  10538  ondomon  10600  axrepnd  10631  fpwwe2lem11  10678  genpcd  11043  ltexprlem6  11078  axpre-sup  11206  negf1o  11690  recex  11892  uzaddcl  12943  nn01to3  12980  rpnnen1lem5  13020  xrsupsslem  13345  xrinfmsslem  13346  supxrunb1  13357  supxrunb2  13358  fz0fzelfz0  13670  fz0fzdiffz0  13673  elfzmlbp  13675  difelfzle  13677  fzo1fzo0n0  13750  elincfzoext  13758  ssfzo12bi  13796  elfznelfzo  13807  modaddmodup  13971  modfzo0difsn  13980  fsuppmapnn0fiubex  14029  seqf1o  14080  expcllem  14109  expeq0  14129  mulexp  14138  hashgt12el2  14458  hashimarni  14476  hash2prd  14510  fi1uzind  14542  swrdnd  14688  swrdswrdlem  14738  swrdswrd  14739  pfxccat3  14768  reuccatpfxs1  14781  repswswrd  14818  repswccat  14820  cshwidxmod  14837  2cshwcshw  14860  s4f1o  14953  wwlktovfo  14993  relexpindlem  15098  resqrex  15285  summo  15749  fsum2d  15803  modfsummods  15825  binom  15862  clim2prod  15920  fprod2d  16013  binomfallfac  16073  efexp  16133  demoivreALT  16233  divconjdvds  16348  addmodlteqALT  16358  dfgcd2  16579  lcmfunsnlem2lem1  16671  lcmfdvdsb  16676  lcmfun  16678  coprmprod  16694  coprmproddvdslem  16695  oddprmdvds  16936  ramcl  17062  prmgaplem6  17089  cshwsidrepswmod0  17128  cshwshashlem1  17129  cshwshashlem2  17130  ressress  17293  initoeu2lem1  18067  symggen  19502  pmtr3ncom  19507  srgmulgass  20234  srgbinom  20248  ringinvnzdiv  20314  rhmsubcrngclem2  20683  lmodvsmmulgdi  20911  nzerooringczr  21508  psgndiflemB  21635  assamulgscmlem2  21937  mptcoe1fsupp  22232  coe1fzgsumdlem  22322  evl1gsumdlem  22375  scmatmulcl  22539  mdetdiagid  22621  pm2mpf1  22820  mptcoe1matfsupp  22823  mp2pm2mplem4  22830  chpdmat  22862  chfacfisf  22875  chfacfisfcpmat  22876  chcoeffeq  22907  topbas  22994  elcls  23096  elcls3  23106  2ndcdisj  23479  filufint  23943  ovoliunlem3  25552  dvge0  26059  ulmcn  26456  gausslemma2dlem3  27426  nosupbnd1  27773  nosupbnd2  27775  noinfbnd1  27788  noinfbnd2  27790  sizusglecusg  29495  upgriswlk  29673  2pthnloop  29763  crctcshwlkn0  29850  wlknwwlksnbij  29917  wwlksnred  29921  wwlksnext  29922  wwlksnextinj  29928  wwlksnextproplem2  29939  wwlksnextproplem3  29940  usgr2wspthons3  29993  clwwlkccatlem  30017  clwlkclwwlklem2a4  30025  clwlkclwwlklem2a  30026  clwlkclwwlklem2  30028  erclwwlktr  30050  clwwlkinwwlk  30068  clwwlkf  30075  clwwlkf1  30077  wwlksext2clwwlk  30085  clwwlknscsh  30090  umgr2cwwk2dif  30092  erclwwlkntr  30099  clwwlknonex2  30137  uhgr3cyclex  30210  upgr4cycl4dv4e  30213  eucrctshift  30271  3cyclfrgrrn1  30313  frgrwopreglem2  30341  frgrwopreglem5  30349  frgrwopreglem5ALT  30350  numclwwlk1lem2fo  30386  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  frgrreg  30422  friendshipgt3  30426  friendship  30427  ipasslem1  30859  shmodsi  31417  elspansn5  31602  h1datomi  31609  nmopsetretALT  31891  pjss2coi  32192  pj3cor1i  32237  mdexchi  32363  atcvat4i  32425  mdsymlem3  32433  mdsymlem4  32434  sumdmdii  32443  cdj3lem2b  32465  elabreximd  32537  iuninc  32580  iundisjf  32608  xrsmulgzz  32993  gsumle  33083  gsumvsca1  33214  gsumvsca2  33215  ofldchr  33323  unitprodclb  33396  rprmdvdsprod  33541  1arithidom  33544  constrmon  33748  locfinreflem  33800  xrge0iifiso  33895  lmxrge0  33912  esumfzf  34049  sigaclfu2  34101  signstfvneq0  34565  satfrel  35351  satfrnmapom  35354  fmlafvel  35369  fmlasuc  35370  bccolsum  35718  faclimlem1  35722  segletr  36095  segleantisym  36096  outsideoftr  36110  exp5d  36284  elicc3  36299  finxpreclem2  37372  wl-sbcom2d  37541  poimirlem26  37632  mblfinlem3  37645  itg2addnc  37660  indexa  37719  disjlem19  38782  ax12indalem  38926  ax12inda2ALT  38927  cvrat4  39425  elpaddn0  39782  paddasslem5  39806  paddasslem14  39815  eldioph2  42749  pell1234qrdich  42848  oaabsb  43283  onmcl  43320  tfsconcat0b  43335  oaun3lem1  43363  oaun3lem2  43364  naddgeoa  43383  gneispb  44120  rexlimd3  45083  rexabslelem  45367  climsuselem1  45562  stoweidlem19  45974  stoweidlem20  45975  stoweidlem34  45989  wallispilem3  46022  sge0iunmpt  46373  meaiuninc3v  46439  smflimmpt  46765  or2expropbilem1  46981  fsetprcnexALT  47011  2reu8i  47062  2elfz2melfz  47267  subsubelfzo0  47275  iccpartigtl  47347  iccpartgt  47351  icceuelpartlem  47359  fargshiftf1  47365  ich2exprop  47395  ichreuopeq  47397  lighneallem3  47531  gbowgt5  47686  bgoldbtbndlem3  47731  bgoldbtbndlem4  47732  bgoldbtbnd  47733  tgblthelfgott  47739  isuspgrimlem  47811  grimco  47817  grimedg  47840  upgrwlkupwlk  47983  2zrngagrp  48092  lmodvsmdi  48223  ply1mulgsumlem1  48231  elfzolborelfzop1  48364  nnolog2flm1  48439  nn0sumshdiglemA  48468  eenglngeehlnmlem2  48587