Theorem exp31 425

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 418	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	ex 418	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  exp41  440  exp42  441  imp5a  446  expl  463  anasss  472  an31s  667  exbiri  823  3exp  1137  exp516  1375  rexlimdva2  3167  r19.29af2  3272  reusv2lem2  5368  pwssun  5551  onmindif  6456  mpteqb  7010  dffo3f  7103  fompt  7115  fliftfun  7317  elovmpt3rab1  7678  ordsucss  7818  tfindsg  7861  tfrlem1  8368  tfrlem9  8378  oaordi  8537  oaordex  8549  oaass  8552  oarec  8553  omass  8571  oen0  8578  oeordsuc  8586  nnaordi  8610  omsmolem  8649  naddssim  8678  brinxper  8730  infensuc  9157  suppeqfsuppbi  9353  marypha1lem  9407  hartogs  9520  card2on  9530  tz9.12lem3  9775  infxpenlem  10020  cfcoflem  10278  isf32lem12  10370  zorn2lem6  10507  ondomon  10575  axrepnd  10607  fpwwe2lem11  10654  genpcd  11019  ltexprlem6  11054  axpre-sup  11182  negf1o  11672  recex  11874  uzaddcl  12957  nn01to3  12994  rpnnen1lem5  13035  xrsupsslem  13363  xrinfmsslem  13364  supxrunb1  13375  supxrunb2  13376  fz0fzelfz0  13693  fz0fzdiffz0  13696  elfzmlbp  13698  difelfzle  13700  fzo1fzo0n0  13775  elincfzoext  13783  ssfzo12bi  13821  elfznelfzo  13833  modaddmodup  14002  modfzo0difsn  14011  fsuppmapnn0fiubex  14060  seqf1o  14111  expcllem  14140  expeq0  14160  mulexp  14169  hashgt12el2  14492  hashimarni  14510  hash2prd  14544  fi1uzind  14576  swrdnd  14728  swrdswrdlem  14777  swrdswrd  14778  pfxccat3  14807  reuccatpfxs1  14820  repswswrd  14859  repswccat  14861  cshwidxmod  14878  2cshwcshw  14900  s4f1o  14993  wwlktovfo  15035  relexpindlem  15140  resqrex  15341  summo  15807  fsum2d  15861  modfsummods  15884  binom  15923  clim2prod  15981  fprod2d  16074  binomfallfac  16133  efexp  16195  demoivreALT  16295  divconjdvds  16411  addmodlteqALT  16421  dfgcd2  16642  lcmfunsnlem2lem1  16734  lcmfdvdsb  16739  lcmfun  16741  coprmprod  16757  coprmproddvdslem  16758  oddprmdvds  17001  ramcl  17127  prmgaplem6  17154  cshwsidrepswmod0  17192  cshwshashlem1  17193  cshwshashlem2  17194  ressress  17345  initoeu2lem1  18109  mgmn0plusgplusf  18748  symggen  19603  pmtr3ncom  19608  gsumle  20278  srgmulgass  20362  srgbinom  20376  ringinvnzdiv  20449  rhmsubcrngclem2  20835  lmodvsmmulgdi  21087  nzerooringczr  21699  ofldchr  21795  psgndiflemB  21819  assamulgscmlem2  22121  mptcoe1fsupp  22446  coe1fzgsumdlem  22534  evl1gsumdlem  22587  scmatmulcl  22746  mdetdiagid  22828  pm2mpf1  23030  mptcoe1matfsupp  23033  mp2pm2mplem4  23040  chpdmat  23072  chfacfisf  23085  chfacfisfcpmat  23086  chcoeffeq  23117  topbas  23203  elcls  23304  elcls3  23314  2ndcdisj  23688  filufint  24152  ovoliunlem3  25738  dvge0  26240  ulmcn  26642  gausslemma2dlem3  27612  nosupbnd1  27958  nosupbnd2  27960  noinfbnd1  27973  noinfbnd2  27975  sizusglecusg  29931  upgriswlk  30108  2pthnloop  30204  crctcshwlkn0  30297  wlknwwlksnbij  30364  wwlksnred  30368  wwlksnext  30369  wwlksnextinj  30375  wwlksnextproplem2  30386  wwlksnextproplem3  30387  usgr2wspthons3  30443  clwwlkccatlem  30467  clwlkclwwlklem2a4  30475  clwlkclwwlklem2a  30476  clwlkclwwlklem2  30478  erclwwlktr  30500  clwwlkinwwlk  30518  clwwlkf  30525  clwwlkf1  30527  wwlksext2clwwlk  30535  clwwlknscsh  30540  umgr2cwwk2dif  30542  erclwwlkntr  30549  clwwlknonex2  30587  uhgr3cyclex  30670  upgr4cycl4dv4e  30673  eucrctshift  30731  3cyclfrgrrn1  30773  frgrwopreglem2  30801  frgrwopreglem5  30809  frgrwopreglem5ALT  30810  numclwwlk1lem2fo  30846  numclwlk2lem2f  30865  numclwlk2lem2f1o  30867  frgrreg  30882  friendshipgt3  30886  friendship  30887  ipasslem1  31320  shmodsi  31878  elspansn5  32063  h1datomi  32070  nmopsetretALT  32352  pjss2coi  32653  pj3cor1i  32698  mdexchi  32824  atcvat4i  32886  mdsymlem3  32894  mdsymlem4  32895  sumdmdii  32904  cdj3lem2b  32926  elabreximd  32993  iuninc  33042  iundisjf  33070  xrsmulgzz  33457  gsumvsca1  33674  gsumvsca2  33675  unitprodclb  33830  rprmdvdsprod  33952  1arithidom  33955  constrmon  34262  locfinreflem  34358  xrge0iifiso  34453  lmxrge0  34470  esumfzf  34587  sigaclfu2  34639  signstfvneq0  35088  satfrel  35954  satfrnmapom  35957  fmlafvel  35972  fmlasuc  35973  bccolsum  36326  faclimlem1  36330  segletr  36702  segleantisym  36703  outsideoftr  36717  exp5d  36930  elicc3  36944  finxpreclem2  38152  wl-sbcom2d  38332  poimirlem26  38403  mblfinlem3  38416  itg2addnc  38431  indexa  38491  disjlem19  39660  ax12indalem  39826  ax12inda2ALT  39827  cvrat4  40324  elpaddn0  40681  paddasslem5  40705  paddasslem14  40714  eldioph2  43615  pell1234qrdich  43710  oaabsb  44143  onmcl  44180  tfsconcat0b  44195  oaun3lem1  44223  oaun3lem2  44224  naddgeoa  44243  gneispb  44979  rexlimd3  45984  rexabslelem  46254  climsuselem1  46445  stoweidlem19  46855  stoweidlem20  46856  stoweidlem34  46870  wallispilem3  46903  sge0iunmpt  47254  meaiuninc3v  47320  smflimmpt  47646  or2expropbilem1  47928  fsetprcnexALT  47958  2reu8i  48009  2elfz2melfz  48214  subsubelfzo0  48223  iccpartigtl  48331  iccpartgt  48335  icceuelpartlem  48343  fargshiftf1  48349  ich2exprop  48379  ichreuopeq  48381  lighneallem3  48518  gbowgt5  48686  bgoldbtbndlem3  48731  bgoldbtbndlem4  48732  bgoldbtbnd  48733  tgblthelfgott  48739  grimco  48813  isuspgrimlem  48819  grimedg  48859  upgrwlkupwlk  49064  2zrngagrp  49172  lmodvsmdi  49317  ply1mulgsumlem1  49324  elfzolborelfzop1  49457  nnolog2flm1  49528  nn0sumshdiglemA  49557  eenglngeehlnmlem2  49676