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  811  3exp  1120  exp516  1357  rexlimdva2  3157  r19.29af2  3267  reusv2lem2  5399  pwssun  5575  onmindif  6476  mpteqb  7035  dffo3f  7126  fompt  7138  fliftfun  7332  elovmpt3rab1  7693  ordsucss  7838  tfindsg  7882  tfrlem1  8416  tfrlem9  8425  oaordi  8584  oaordex  8596  oaass  8599  oarec  8600  omass  8618  oen0  8624  oeordsuc  8632  nnaordi  8656  omsmolem  8695  naddssim  8723  brinxper  8774  infensuc  9195  php3OLD  9261  suppeqfsuppbi  9419  marypha1lem  9473  hartogs  9584  card2on  9594  tz9.12lem3  9829  infxpenlem  10053  cfcoflem  10312  isf32lem12  10404  zorn2lem6  10541  ondomon  10603  axrepnd  10634  fpwwe2lem11  10681  genpcd  11046  ltexprlem6  11081  axpre-sup  11209  negf1o  11693  recex  11895  uzaddcl  12946  nn01to3  12983  rpnnen1lem5  13023  xrsupsslem  13349  xrinfmsslem  13350  supxrunb1  13361  supxrunb2  13362  fz0fzelfz0  13674  fz0fzdiffz0  13677  elfzmlbp  13679  difelfzle  13681  fzo1fzo0n0  13754  elincfzoext  13762  ssfzo12bi  13800  elfznelfzo  13811  modaddmodup  13975  modfzo0difsn  13984  fsuppmapnn0fiubex  14033  seqf1o  14084  expcllem  14113  expeq0  14133  mulexp  14142  hashgt12el2  14462  hashimarni  14480  hash2prd  14514  fi1uzind  14546  swrdnd  14692  swrdswrdlem  14742  swrdswrd  14743  pfxccat3  14772  reuccatpfxs1  14785  repswswrd  14822  repswccat  14824  cshwidxmod  14841  2cshwcshw  14864  s4f1o  14957  wwlktovfo  14997  relexpindlem  15102  resqrex  15289  summo  15753  fsum2d  15807  modfsummods  15829  binom  15866  clim2prod  15924  fprod2d  16017  binomfallfac  16077  efexp  16137  demoivreALT  16237  divconjdvds  16352  addmodlteqALT  16362  dfgcd2  16583  lcmfunsnlem2lem1  16675  lcmfdvdsb  16680  lcmfun  16682  coprmprod  16698  coprmproddvdslem  16699  oddprmdvds  16941  ramcl  17067  prmgaplem6  17094  cshwsidrepswmod0  17132  cshwshashlem1  17133  cshwshashlem2  17134  ressress  17293  initoeu2lem1  18059  symggen  19488  pmtr3ncom  19493  srgmulgass  20214  srgbinom  20228  ringinvnzdiv  20298  rhmsubcrngclem2  20667  lmodvsmmulgdi  20895  nzerooringczr  21491  psgndiflemB  21618  assamulgscmlem2  21920  mptcoe1fsupp  22217  coe1fzgsumdlem  22307  evl1gsumdlem  22360  scmatmulcl  22524  mdetdiagid  22606  pm2mpf1  22805  mptcoe1matfsupp  22808  mp2pm2mplem4  22815  chpdmat  22847  chfacfisf  22860  chfacfisfcpmat  22861  chcoeffeq  22892  topbas  22979  elcls  23081  elcls3  23091  2ndcdisj  23464  filufint  23928  ovoliunlem3  25539  dvge0  26045  ulmcn  26442  gausslemma2dlem3  27412  nosupbnd1  27759  nosupbnd2  27761  noinfbnd1  27774  noinfbnd2  27776  sizusglecusg  29481  upgriswlk  29659  2pthnloop  29751  crctcshwlkn0  29841  wlknwwlksnbij  29908  wwlksnred  29912  wwlksnext  29913  wwlksnextinj  29919  wwlksnextproplem2  29930  wwlksnextproplem3  29931  usgr2wspthons3  29984  clwwlkccatlem  30008  clwlkclwwlklem2a4  30016  clwlkclwwlklem2a  30017  clwlkclwwlklem2  30019  erclwwlktr  30041  clwwlkinwwlk  30059  clwwlkf  30066  clwwlkf1  30068  wwlksext2clwwlk  30076  clwwlknscsh  30081  umgr2cwwk2dif  30083  erclwwlkntr  30090  clwwlknonex2  30128  uhgr3cyclex  30201  upgr4cycl4dv4e  30204  eucrctshift  30262  3cyclfrgrrn1  30304  frgrwopreglem2  30332  frgrwopreglem5  30340  frgrwopreglem5ALT  30341  numclwwlk1lem2fo  30377  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  frgrreg  30413  friendshipgt3  30417  friendship  30418  ipasslem1  30850  shmodsi  31408  elspansn5  31593  h1datomi  31600  nmopsetretALT  31882  pjss2coi  32183  pj3cor1i  32228  mdexchi  32354  atcvat4i  32416  mdsymlem3  32424  mdsymlem4  32425  sumdmdii  32434  cdj3lem2b  32456  elabreximd  32529  iuninc  32573  iundisjf  32602  xrsmulgzz  33011  gsumle  33101  gsumvsca1  33232  gsumvsca2  33233  ofldchr  33344  unitprodclb  33417  rprmdvdsprod  33562  1arithidom  33565  constrmon  33785  locfinreflem  33839  xrge0iifiso  33934  lmxrge0  33951  esumfzf  34070  sigaclfu2  34122  signstfvneq0  34587  satfrel  35372  satfrnmapom  35375  fmlafvel  35390  fmlasuc  35391  bccolsum  35739  faclimlem1  35743  segletr  36115  segleantisym  36116  outsideoftr  36130  exp5d  36303  elicc3  36318  finxpreclem2  37391  wl-sbcom2d  37562  poimirlem26  37653  mblfinlem3  37666  itg2addnc  37681  indexa  37740  disjlem19  38802  ax12indalem  38946  ax12inda2ALT  38947  cvrat4  39445  elpaddn0  39802  paddasslem5  39826  paddasslem14  39835  eldioph2  42773  pell1234qrdich  42872  oaabsb  43307  onmcl  43344  tfsconcat0b  43359  oaun3lem1  43387  oaun3lem2  43388  naddgeoa  43407  gneispb  44144  rexlimd3  45149  rexabslelem  45429  climsuselem1  45622  stoweidlem19  46034  stoweidlem20  46035  stoweidlem34  46049  wallispilem3  46082  sge0iunmpt  46433  meaiuninc3v  46499  smflimmpt  46825  or2expropbilem1  47044  fsetprcnexALT  47074  2reu8i  47125  2elfz2melfz  47330  subsubelfzo0  47338  iccpartigtl  47410  iccpartgt  47414  icceuelpartlem  47422  fargshiftf1  47428  ich2exprop  47458  ichreuopeq  47460  lighneallem3  47594  gbowgt5  47749  bgoldbtbndlem3  47794  bgoldbtbndlem4  47795  bgoldbtbnd  47796  tgblthelfgott  47802  isuspgrimlem  47874  grimco  47880  grimedg  47903  upgrwlkupwlk  48056  2zrngagrp  48165  lmodvsmdi  48295  ply1mulgsumlem1  48303  elfzolborelfzop1  48436  nnolog2flm1  48511  nn0sumshdiglemA  48540  eenglngeehlnmlem2  48659