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  810  3exp  1119  exp516  1357  rexlimdva2  3139  r19.29af2  3244  reusv2lem2  5344  pwssun  5516  onmindif  6411  mpteqb  6960  dffo3f  7051  fompt  7063  fliftfun  7258  elovmpt3rab1  7618  ordsucss  7760  tfindsg  7803  tfrlem1  8307  tfrlem9  8316  oaordi  8473  oaordex  8485  oaass  8488  oarec  8489  omass  8507  oen0  8514  oeordsuc  8522  nnaordi  8546  omsmolem  8585  naddssim  8613  brinxper  8664  infensuc  9083  suppeqfsuppbi  9282  marypha1lem  9336  hartogs  9449  card2on  9459  tz9.12lem3  9701  infxpenlem  9923  cfcoflem  10182  isf32lem12  10274  zorn2lem6  10411  ondomon  10473  axrepnd  10505  fpwwe2lem11  10552  genpcd  10917  ltexprlem6  10952  axpre-sup  11080  negf1o  11567  recex  11769  uzaddcl  12817  nn01to3  12854  rpnnen1lem5  12894  xrsupsslem  13222  xrinfmsslem  13223  supxrunb1  13234  supxrunb2  13235  fz0fzelfz0  13550  fz0fzdiffz0  13553  elfzmlbp  13555  difelfzle  13557  fzo1fzo0n0  13631  elincfzoext  13639  ssfzo12bi  13677  elfznelfzo  13689  modaddmodup  13857  modfzo0difsn  13866  fsuppmapnn0fiubex  13915  seqf1o  13966  expcllem  13995  expeq0  14015  mulexp  14024  hashgt12el2  14346  hashimarni  14364  hash2prd  14398  fi1uzind  14430  swrdnd  14578  swrdswrdlem  14627  swrdswrd  14628  pfxccat3  14657  reuccatpfxs1  14670  repswswrd  14707  repswccat  14709  cshwidxmod  14726  2cshwcshw  14748  s4f1o  14841  wwlktovfo  14881  relexpindlem  14986  resqrex  15173  summo  15640  fsum2d  15694  modfsummods  15716  binom  15753  clim2prod  15811  fprod2d  15904  binomfallfac  15964  efexp  16026  demoivreALT  16126  divconjdvds  16242  addmodlteqALT  16252  dfgcd2  16473  lcmfunsnlem2lem1  16565  lcmfdvdsb  16570  lcmfun  16572  coprmprod  16588  coprmproddvdslem  16589  oddprmdvds  16831  ramcl  16957  prmgaplem6  16984  cshwsidrepswmod0  17022  cshwshashlem1  17023  cshwshashlem2  17024  ressress  17174  initoeu2lem1  17938  symggen  19399  pmtr3ncom  19404  gsumle  20074  srgmulgass  20152  srgbinom  20166  ringinvnzdiv  20236  rhmsubcrngclem2  20600  lmodvsmmulgdi  20848  nzerooringczr  21435  ofldchr  21531  psgndiflemB  21555  assamulgscmlem2  21856  mptcoe1fsupp  22156  coe1fzgsumdlem  22247  evl1gsumdlem  22300  scmatmulcl  22462  mdetdiagid  22544  pm2mpf1  22743  mptcoe1matfsupp  22746  mp2pm2mplem4  22753  chpdmat  22785  chfacfisf  22798  chfacfisfcpmat  22799  chcoeffeq  22830  topbas  22916  elcls  23017  elcls3  23027  2ndcdisj  23400  filufint  23864  ovoliunlem3  25461  dvge0  25967  ulmcn  26364  gausslemma2dlem3  27335  nosupbnd1  27682  nosupbnd2  27684  noinfbnd1  27697  noinfbnd2  27699  sizusglecusg  29537  upgriswlk  29714  2pthnloop  29804  crctcshwlkn0  29894  wlknwwlksnbij  29961  wwlksnred  29965  wwlksnext  29966  wwlksnextinj  29972  wwlksnextproplem2  29983  wwlksnextproplem3  29984  usgr2wspthons3  30040  clwwlkccatlem  30064  clwlkclwwlklem2a4  30072  clwlkclwwlklem2a  30073  clwlkclwwlklem2  30075  erclwwlktr  30097  clwwlkinwwlk  30115  clwwlkf  30122  clwwlkf1  30124  wwlksext2clwwlk  30132  clwwlknscsh  30137  umgr2cwwk2dif  30139  erclwwlkntr  30146  clwwlknonex2  30184  uhgr3cyclex  30257  upgr4cycl4dv4e  30260  eucrctshift  30318  3cyclfrgrrn1  30360  frgrwopreglem2  30388  frgrwopreglem5  30396  frgrwopreglem5ALT  30397  numclwwlk1lem2fo  30433  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  frgrreg  30469  friendshipgt3  30473  friendship  30474  ipasslem1  30906  shmodsi  31464  elspansn5  31649  h1datomi  31656  nmopsetretALT  31938  pjss2coi  32239  pj3cor1i  32284  mdexchi  32410  atcvat4i  32472  mdsymlem3  32480  mdsymlem4  32481  sumdmdii  32490  cdj3lem2b  32512  elabreximd  32585  iuninc  32635  iundisjf  32664  xrsmulgzz  33091  gsumvsca1  33308  gsumvsca2  33309  unitprodclb  33470  rprmdvdsprod  33615  1arithidom  33618  constrmon  33901  locfinreflem  33997  xrge0iifiso  34092  lmxrge0  34109  esumfzf  34226  sigaclfu2  34278  signstfvneq0  34729  satfrel  35561  satfrnmapom  35564  fmlafvel  35579  fmlasuc  35580  bccolsum  35933  faclimlem1  35937  segletr  36308  segleantisym  36309  outsideoftr  36323  exp5d  36496  elicc3  36511  finxpreclem2  37595  wl-sbcom2d  37766  poimirlem26  37847  mblfinlem3  37860  itg2addnc  37875  indexa  37934  disjlem19  39060  ax12indalem  39205  ax12inda2ALT  39206  cvrat4  39703  elpaddn0  40060  paddasslem5  40084  paddasslem14  40093  eldioph2  43004  pell1234qrdich  43103  oaabsb  43536  onmcl  43573  tfsconcat0b  43588  oaun3lem1  43616  oaun3lem2  43617  naddgeoa  43636  gneispb  44372  rexlimd3  45388  rexabslelem  45662  climsuselem1  45853  stoweidlem19  46263  stoweidlem20  46264  stoweidlem34  46278  wallispilem3  46311  sge0iunmpt  46662  meaiuninc3v  46728  smflimmpt  47054  or2expropbilem1  47278  fsetprcnexALT  47308  2reu8i  47359  2elfz2melfz  47564  subsubelfzo0  47572  iccpartigtl  47669  iccpartgt  47673  icceuelpartlem  47681  fargshiftf1  47687  ich2exprop  47717  ichreuopeq  47719  lighneallem3  47853  gbowgt5  48008  bgoldbtbndlem3  48053  bgoldbtbndlem4  48054  bgoldbtbnd  48055  tgblthelfgott  48061  grimco  48135  isuspgrimlem  48141  grimedg  48181  upgrwlkupwlk  48386  2zrngagrp  48495  lmodvsmdi  48625  ply1mulgsumlem1  48632  elfzolborelfzop1  48765  nnolog2flm1  48836  nn0sumshdiglemA  48865  eenglngeehlnmlem2  48984