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  655  exbiri  811  3exp  1120  exp516  1358  rexlimdva2  3141  r19.29af2  3246  reusv2lem2  5346  pwssun  5524  onmindif  6419  mpteqb  6969  dffo3f  7060  fompt  7072  fliftfun  7268  elovmpt3rab1  7628  ordsucss  7770  tfindsg  7813  tfrlem1  8317  tfrlem9  8326  oaordi  8483  oaordex  8495  oaass  8498  oarec  8499  omass  8517  oen0  8524  oeordsuc  8532  nnaordi  8556  omsmolem  8595  naddssim  8623  brinxper  8675  infensuc  9095  suppeqfsuppbi  9294  marypha1lem  9348  hartogs  9461  card2on  9471  tz9.12lem3  9713  infxpenlem  9935  cfcoflem  10194  isf32lem12  10286  zorn2lem6  10423  ondomon  10485  axrepnd  10517  fpwwe2lem11  10564  genpcd  10929  ltexprlem6  10964  axpre-sup  11092  negf1o  11579  recex  11781  uzaddcl  12829  nn01to3  12866  rpnnen1lem5  12906  xrsupsslem  13234  xrinfmsslem  13235  supxrunb1  13246  supxrunb2  13247  fz0fzelfz0  13562  fz0fzdiffz0  13565  elfzmlbp  13567  difelfzle  13569  fzo1fzo0n0  13643  elincfzoext  13651  ssfzo12bi  13689  elfznelfzo  13701  modaddmodup  13869  modfzo0difsn  13878  fsuppmapnn0fiubex  13927  seqf1o  13978  expcllem  14007  expeq0  14027  mulexp  14036  hashgt12el2  14358  hashimarni  14376  hash2prd  14410  fi1uzind  14442  swrdnd  14590  swrdswrdlem  14639  swrdswrd  14640  pfxccat3  14669  reuccatpfxs1  14682  repswswrd  14719  repswccat  14721  cshwidxmod  14738  2cshwcshw  14760  s4f1o  14853  wwlktovfo  14893  relexpindlem  14998  resqrex  15185  summo  15652  fsum2d  15706  modfsummods  15728  binom  15765  clim2prod  15823  fprod2d  15916  binomfallfac  15976  efexp  16038  demoivreALT  16138  divconjdvds  16254  addmodlteqALT  16264  dfgcd2  16485  lcmfunsnlem2lem1  16577  lcmfdvdsb  16582  lcmfun  16584  coprmprod  16600  coprmproddvdslem  16601  oddprmdvds  16843  ramcl  16969  prmgaplem6  16996  cshwsidrepswmod0  17034  cshwshashlem1  17035  cshwshashlem2  17036  ressress  17186  initoeu2lem1  17950  symggen  19411  pmtr3ncom  19416  gsumle  20086  srgmulgass  20164  srgbinom  20178  ringinvnzdiv  20248  rhmsubcrngclem2  20612  lmodvsmmulgdi  20860  nzerooringczr  21447  ofldchr  21543  psgndiflemB  21567  assamulgscmlem2  21868  mptcoe1fsupp  22168  coe1fzgsumdlem  22259  evl1gsumdlem  22312  scmatmulcl  22474  mdetdiagid  22556  pm2mpf1  22755  mptcoe1matfsupp  22758  mp2pm2mplem4  22765  chpdmat  22797  chfacfisf  22810  chfacfisfcpmat  22811  chcoeffeq  22842  topbas  22928  elcls  23029  elcls3  23039  2ndcdisj  23412  filufint  23876  ovoliunlem3  25473  dvge0  25979  ulmcn  26376  gausslemma2dlem3  27347  nosupbnd1  27694  nosupbnd2  27696  noinfbnd1  27709  noinfbnd2  27711  sizusglecusg  29549  upgriswlk  29726  2pthnloop  29816  crctcshwlkn0  29906  wlknwwlksnbij  29973  wwlksnred  29977  wwlksnext  29978  wwlksnextinj  29984  wwlksnextproplem2  29995  wwlksnextproplem3  29996  usgr2wspthons3  30052  clwwlkccatlem  30076  clwlkclwwlklem2a4  30084  clwlkclwwlklem2a  30085  clwlkclwwlklem2  30087  erclwwlktr  30109  clwwlkinwwlk  30127  clwwlkf  30134  clwwlkf1  30136  wwlksext2clwwlk  30144  clwwlknscsh  30149  umgr2cwwk2dif  30151  erclwwlkntr  30158  clwwlknonex2  30196  uhgr3cyclex  30269  upgr4cycl4dv4e  30272  eucrctshift  30330  3cyclfrgrrn1  30372  frgrwopreglem2  30400  frgrwopreglem5  30408  frgrwopreglem5ALT  30409  numclwwlk1lem2fo  30445  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  frgrreg  30481  friendshipgt3  30485  friendship  30486  ipasslem1  30918  shmodsi  31476  elspansn5  31661  h1datomi  31668  nmopsetretALT  31950  pjss2coi  32251  pj3cor1i  32296  mdexchi  32422  atcvat4i  32484  mdsymlem3  32492  mdsymlem4  32493  sumdmdii  32502  cdj3lem2b  32524  elabreximd  32596  iuninc  32646  iundisjf  32675  xrsmulgzz  33101  gsumvsca1  33319  gsumvsca2  33320  unitprodclb  33481  rprmdvdsprod  33626  1arithidom  33629  constrmon  33921  locfinreflem  34017  xrge0iifiso  34112  lmxrge0  34129  esumfzf  34246  sigaclfu2  34298  signstfvneq0  34749  satfrel  35580  satfrnmapom  35583  fmlafvel  35598  fmlasuc  35599  bccolsum  35952  faclimlem1  35956  segletr  36327  segleantisym  36328  outsideoftr  36342  exp5d  36515  elicc3  36530  finxpreclem2  37642  wl-sbcom2d  37813  poimirlem26  37894  mblfinlem3  37907  itg2addnc  37922  indexa  37981  disjlem19  39152  ax12indalem  39318  ax12inda2ALT  39319  cvrat4  39816  elpaddn0  40173  paddasslem5  40197  paddasslem14  40206  eldioph2  43116  pell1234qrdich  43215  oaabsb  43648  onmcl  43685  tfsconcat0b  43700  oaun3lem1  43728  oaun3lem2  43729  naddgeoa  43748  gneispb  44484  rexlimd3  45500  rexabslelem  45773  climsuselem1  45964  stoweidlem19  46374  stoweidlem20  46375  stoweidlem34  46389  wallispilem3  46422  sge0iunmpt  46773  meaiuninc3v  46839  smflimmpt  47165  or2expropbilem1  47389  fsetprcnexALT  47419  2reu8i  47470  2elfz2melfz  47675  subsubelfzo0  47683  iccpartigtl  47780  iccpartgt  47784  icceuelpartlem  47792  fargshiftf1  47798  ich2exprop  47828  ichreuopeq  47830  lighneallem3  47964  gbowgt5  48119  bgoldbtbndlem3  48164  bgoldbtbndlem4  48165  bgoldbtbnd  48166  tgblthelfgott  48172  grimco  48246  isuspgrimlem  48252  grimedg  48292  upgrwlkupwlk  48497  2zrngagrp  48606  lmodvsmdi  48736  ply1mulgsumlem1  48743  elfzolborelfzop1  48876  nnolog2flm1  48947  nn0sumshdiglemA  48976  eenglngeehlnmlem2  49095