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  5336  pwssun  5516  onmindif  6411  mpteqb  6961  dffo3f  7052  fompt  7064  fliftfun  7260  elovmpt3rab1  7620  ordsucss  7762  tfindsg  7805  tfrlem1  8308  tfrlem9  8317  oaordi  8474  oaordex  8486  oaass  8489  oarec  8490  omass  8508  oen0  8515  oeordsuc  8523  nnaordi  8547  omsmolem  8586  naddssim  8614  brinxper  8666  infensuc  9086  suppeqfsuppbi  9285  marypha1lem  9339  hartogs  9452  card2on  9462  tz9.12lem3  9704  infxpenlem  9926  cfcoflem  10185  isf32lem12  10277  zorn2lem6  10414  ondomon  10476  axrepnd  10508  fpwwe2lem11  10555  genpcd  10920  ltexprlem6  10955  axpre-sup  11083  negf1o  11571  recex  11773  uzaddcl  12845  nn01to3  12882  rpnnen1lem5  12922  xrsupsslem  13250  xrinfmsslem  13251  supxrunb1  13262  supxrunb2  13263  fz0fzelfz0  13579  fz0fzdiffz0  13582  elfzmlbp  13584  difelfzle  13586  fzo1fzo0n0  13661  elincfzoext  13669  ssfzo12bi  13707  elfznelfzo  13719  modaddmodup  13887  modfzo0difsn  13896  fsuppmapnn0fiubex  13945  seqf1o  13996  expcllem  14025  expeq0  14045  mulexp  14054  hashgt12el2  14376  hashimarni  14394  hash2prd  14428  fi1uzind  14460  swrdnd  14608  swrdswrdlem  14657  swrdswrd  14658  pfxccat3  14687  reuccatpfxs1  14700  repswswrd  14737  repswccat  14739  cshwidxmod  14756  2cshwcshw  14778  s4f1o  14871  wwlktovfo  14911  relexpindlem  15016  resqrex  15203  summo  15670  fsum2d  15724  modfsummods  15747  binom  15786  clim2prod  15844  fprod2d  15937  binomfallfac  15997  efexp  16059  demoivreALT  16159  divconjdvds  16275  addmodlteqALT  16285  dfgcd2  16506  lcmfunsnlem2lem1  16598  lcmfdvdsb  16603  lcmfun  16605  coprmprod  16621  coprmproddvdslem  16622  oddprmdvds  16865  ramcl  16991  prmgaplem6  17018  cshwsidrepswmod0  17056  cshwshashlem1  17057  cshwshashlem2  17058  ressress  17208  initoeu2lem1  17972  symggen  19436  pmtr3ncom  19441  gsumle  20111  srgmulgass  20189  srgbinom  20203  ringinvnzdiv  20273  rhmsubcrngclem2  20635  lmodvsmmulgdi  20883  nzerooringczr  21470  ofldchr  21566  psgndiflemB  21590  assamulgscmlem2  21890  mptcoe1fsupp  22189  coe1fzgsumdlem  22278  evl1gsumdlem  22331  scmatmulcl  22493  mdetdiagid  22575  pm2mpf1  22774  mptcoe1matfsupp  22777  mp2pm2mplem4  22784  chpdmat  22816  chfacfisf  22829  chfacfisfcpmat  22830  chcoeffeq  22861  topbas  22947  elcls  23048  elcls3  23058  2ndcdisj  23431  filufint  23895  ovoliunlem3  25481  dvge0  25983  ulmcn  26377  gausslemma2dlem3  27345  nosupbnd1  27692  nosupbnd2  27694  noinfbnd1  27707  noinfbnd2  27709  sizusglecusg  29547  upgriswlk  29724  2pthnloop  29814  crctcshwlkn0  29904  wlknwwlksnbij  29971  wwlksnred  29975  wwlksnext  29976  wwlksnextinj  29982  wwlksnextproplem2  29993  wwlksnextproplem3  29994  usgr2wspthons3  30050  clwwlkccatlem  30074  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  clwlkclwwlklem2  30085  erclwwlktr  30107  clwwlkinwwlk  30125  clwwlkf  30132  clwwlkf1  30134  wwlksext2clwwlk  30142  clwwlknscsh  30147  umgr2cwwk2dif  30149  erclwwlkntr  30156  clwwlknonex2  30194  uhgr3cyclex  30267  upgr4cycl4dv4e  30270  eucrctshift  30328  3cyclfrgrrn1  30370  frgrwopreglem2  30398  frgrwopreglem5  30406  frgrwopreglem5ALT  30407  numclwwlk1lem2fo  30443  numclwlk2lem2f  30462  numclwlk2lem2f1o  30464  frgrreg  30479  friendshipgt3  30483  friendship  30484  ipasslem1  30917  shmodsi  31475  elspansn5  31660  h1datomi  31667  nmopsetretALT  31949  pjss2coi  32250  pj3cor1i  32295  mdexchi  32421  atcvat4i  32483  mdsymlem3  32491  mdsymlem4  32492  sumdmdii  32501  cdj3lem2b  32523  elabreximd  32595  iuninc  32645  iundisjf  32674  xrsmulgzz  33084  gsumvsca1  33302  gsumvsca2  33303  unitprodclb  33464  rprmdvdsprod  33609  1arithidom  33612  constrmon  33904  locfinreflem  34000  xrge0iifiso  34095  lmxrge0  34112  esumfzf  34229  sigaclfu2  34281  signstfvneq0  34732  satfrel  35565  satfrnmapom  35568  fmlafvel  35583  fmlasuc  35584  bccolsum  35937  faclimlem1  35941  segletr  36312  segleantisym  36313  outsideoftr  36327  exp5d  36500  elicc3  36515  finxpreclem2  37720  wl-sbcom2d  37900  poimirlem26  37981  mblfinlem3  37994  itg2addnc  38009  indexa  38068  disjlem19  39239  ax12indalem  39405  ax12inda2ALT  39406  cvrat4  39903  elpaddn0  40260  paddasslem5  40284  paddasslem14  40293  eldioph2  43208  pell1234qrdich  43307  oaabsb  43740  onmcl  43777  tfsconcat0b  43792  oaun3lem1  43820  oaun3lem2  43821  naddgeoa  43840  gneispb  44576  rexlimd3  45592  rexabslelem  45864  climsuselem1  46055  stoweidlem19  46465  stoweidlem20  46466  stoweidlem34  46480  wallispilem3  46513  sge0iunmpt  46864  meaiuninc3v  46930  smflimmpt  47256  or2expropbilem1  47492  fsetprcnexALT  47522  2reu8i  47573  2elfz2melfz  47778  subsubelfzo0  47787  iccpartigtl  47895  iccpartgt  47899  icceuelpartlem  47907  fargshiftf1  47913  ich2exprop  47943  ichreuopeq  47945  lighneallem3  48082  gbowgt5  48250  bgoldbtbndlem3  48295  bgoldbtbndlem4  48296  bgoldbtbnd  48297  tgblthelfgott  48303  grimco  48377  isuspgrimlem  48383  grimedg  48423  upgrwlkupwlk  48628  2zrngagrp  48737  lmodvsmdi  48867  ply1mulgsumlem1  48874  elfzolborelfzop1  49007  nnolog2flm1  49078  nn0sumshdiglemA  49107  eenglngeehlnmlem2  49226