Theorem exp31 420

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  exp41  435  exp42  436  imp5a  441  expl  458  anasss  467  an31s  660  exbiri  816  3exp  1125  exp516  1363  rexlimdva2  3143  r19.29af2  3248  reusv2lem2  5335  pwssun  5517  onmindif  6411  mpteqb  6962  dffo3f  7054  fompt  7066  fliftfun  7263  elovmpt3rab1  7623  ordsucss  7765  tfindsg  7808  tfrlem1  8312  tfrlem9  8321  oaordi  8478  oaordex  8490  oaass  8493  oarec  8494  omass  8512  oen0  8519  oeordsuc  8527  nnaordi  8551  omsmolem  8590  naddssim  8618  brinxper  8670  infensuc  9090  suppeqfsuppbi  9289  marypha1lem  9343  hartogs  9456  card2on  9466  tz9.12lem3  9711  infxpenlem  9933  cfcoflem  10192  isf32lem12  10284  zorn2lem6  10421  ondomon  10483  axrepnd  10515  fpwwe2lem11  10562  genpcd  10927  ltexprlem6  10962  axpre-sup  11090  negf1o  11578  recex  11780  uzaddcl  12852  nn01to3  12889  rpnnen1lem5  12929  xrsupsslem  13257  xrinfmsslem  13258  supxrunb1  13269  supxrunb2  13270  fz0fzelfz0  13586  fz0fzdiffz0  13589  elfzmlbp  13591  difelfzle  13593  fzo1fzo0n0  13668  elincfzoext  13676  ssfzo12bi  13714  elfznelfzo  13726  modaddmodup  13894  modfzo0difsn  13903  fsuppmapnn0fiubex  13952  seqf1o  14003  expcllem  14032  expeq0  14052  mulexp  14061  hashgt12el2  14383  hashimarni  14401  hash2prd  14435  fi1uzind  14467  swrdnd  14615  swrdswrdlem  14664  swrdswrd  14665  pfxccat3  14694  reuccatpfxs1  14707  repswswrd  14744  repswccat  14746  cshwidxmod  14763  2cshwcshw  14785  s4f1o  14878  wwlktovfo  14918  relexpindlem  15023  resqrex  15210  summo  15677  fsum2d  15731  modfsummods  15754  binom  15793  clim2prod  15851  fprod2d  15944  binomfallfac  16004  efexp  16066  demoivreALT  16166  divconjdvds  16282  addmodlteqALT  16292  dfgcd2  16513  lcmfunsnlem2lem1  16605  lcmfdvdsb  16610  lcmfun  16612  coprmprod  16628  coprmproddvdslem  16629  oddprmdvds  16872  ramcl  16998  prmgaplem6  17025  cshwsidrepswmod0  17063  cshwshashlem1  17064  cshwshashlem2  17065  ressress  17215  initoeu2lem1  17979  symggen  19443  pmtr3ncom  19448  gsumle  20118  srgmulgass  20196  srgbinom  20210  ringinvnzdiv  20280  rhmsubcrngclem2  20646  lmodvsmmulgdi  20894  nzerooringczr  21462  ofldchr  21558  psgndiflemB  21582  assamulgscmlem2  21882  mptcoe1fsupp  22207  coe1fzgsumdlem  22296  evl1gsumdlem  22349  scmatmulcl  22508  mdetdiagid  22590  pm2mpf1  22789  mptcoe1matfsupp  22792  mp2pm2mplem4  22799  chpdmat  22831  chfacfisf  22844  chfacfisfcpmat  22845  chcoeffeq  22876  topbas  22962  elcls  23063  elcls3  23073  2ndcdisj  23446  filufint  23910  ovoliunlem3  25496  dvge0  25998  ulmcn  26389  gausslemma2dlem3  27356  nosupbnd1  27703  nosupbnd2  27705  noinfbnd1  27718  noinfbnd2  27720  sizusglecusg  29557  upgriswlk  29734  2pthnloop  29824  crctcshwlkn0  29914  wlknwwlksnbij  29981  wwlksnred  29985  wwlksnext  29986  wwlksnextinj  29992  wwlksnextproplem2  30003  wwlksnextproplem3  30004  usgr2wspthons3  30060  clwwlkccatlem  30084  clwlkclwwlklem2a4  30092  clwlkclwwlklem2a  30093  clwlkclwwlklem2  30095  erclwwlktr  30117  clwwlkinwwlk  30135  clwwlkf  30142  clwwlkf1  30144  wwlksext2clwwlk  30152  clwwlknscsh  30157  umgr2cwwk2dif  30159  erclwwlkntr  30166  clwwlknonex2  30204  uhgr3cyclex  30277  upgr4cycl4dv4e  30280  eucrctshift  30338  3cyclfrgrrn1  30380  frgrwopreglem2  30408  frgrwopreglem5  30416  frgrwopreglem5ALT  30417  numclwwlk1lem2fo  30453  numclwlk2lem2f  30472  numclwlk2lem2f1o  30474  frgrreg  30489  friendshipgt3  30493  friendship  30494  ipasslem1  30927  shmodsi  31485  elspansn5  31670  h1datomi  31677  nmopsetretALT  31959  pjss2coi  32260  pj3cor1i  32305  mdexchi  32431  atcvat4i  32493  mdsymlem3  32501  mdsymlem4  32502  sumdmdii  32511  cdj3lem2b  32533  elabreximd  32605  iuninc  32656  iundisjf  32685  xrsmulgzz  33095  gsumvsca1  33314  gsumvsca2  33315  unitprodclb  33479  rprmdvdsprod  33624  1arithidom  33627  constrmon  33935  locfinreflem  34031  xrge0iifiso  34126  lmxrge0  34143  esumfzf  34260  sigaclfu2  34312  signstfvneq0  34763  satfrel  35602  satfrnmapom  35605  fmlafvel  35620  fmlasuc  35621  bccolsum  35974  faclimlem1  35978  segletr  36349  segleantisym  36350  outsideoftr  36364  exp5d  36537  elicc3  36552  finxpreclem2  37759  wl-sbcom2d  37939  poimirlem26  38020  mblfinlem3  38033  itg2addnc  38048  indexa  38107  disjlem19  39278  ax12indalem  39444  ax12inda2ALT  39445  cvrat4  39942  elpaddn0  40299  paddasslem5  40323  paddasslem14  40332  eldioph2  43218  pell1234qrdich  43313  oaabsb  43746  onmcl  43783  tfsconcat0b  43798  oaun3lem1  43826  oaun3lem2  43827  naddgeoa  43846  gneispb  44582  rexlimd3  45598  rexabslelem  45868  climsuselem1  46059  stoweidlem19  46469  stoweidlem20  46470  stoweidlem34  46484  wallispilem3  46517  sge0iunmpt  46868  meaiuninc3v  46934  smflimmpt  47260  or2expropbilem1  47502  fsetprcnexALT  47532  2reu8i  47583  2elfz2melfz  47788  subsubelfzo0  47797  iccpartigtl  47905  iccpartgt  47909  icceuelpartlem  47917  fargshiftf1  47923  ich2exprop  47953  ichreuopeq  47955  lighneallem3  48092  gbowgt5  48260  bgoldbtbndlem3  48305  bgoldbtbndlem4  48306  bgoldbtbnd  48307  tgblthelfgott  48313  grimco  48387  isuspgrimlem  48393  grimedg  48433  upgrwlkupwlk  48638  2zrngagrp  48747  lmodvsmdi  48877  ply1mulgsumlem1  48884  elfzolborelfzop1  49017  nnolog2flm1  49088  nn0sumshdiglemA  49117  eenglngeehlnmlem2  49236