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  810  3exp  1119  exp516  1357  rexlimdva2  3136  r19.29af2  3241  reusv2lem2  5341  pwssun  5513  onmindif  6407  mpteqb  6956  dffo3f  7047  fompt  7059  fliftfun  7254  elovmpt3rab1  7614  ordsucss  7756  tfindsg  7799  tfrlem1  8303  tfrlem9  8312  oaordi  8469  oaordex  8481  oaass  8484  oarec  8485  omass  8503  oen0  8509  oeordsuc  8517  nnaordi  8541  omsmolem  8580  naddssim  8608  brinxper  8659  infensuc  9077  suppeqfsuppbi  9272  marypha1lem  9326  hartogs  9439  card2on  9449  tz9.12lem3  9691  infxpenlem  9913  cfcoflem  10172  isf32lem12  10264  zorn2lem6  10401  ondomon  10463  axrepnd  10494  fpwwe2lem11  10541  genpcd  10906  ltexprlem6  10941  axpre-sup  11069  negf1o  11556  recex  11758  uzaddcl  12806  nn01to3  12843  rpnnen1lem5  12883  xrsupsslem  13210  xrinfmsslem  13211  supxrunb1  13222  supxrunb2  13223  fz0fzelfz0  13538  fz0fzdiffz0  13541  elfzmlbp  13543  difelfzle  13545  fzo1fzo0n0  13619  elincfzoext  13627  ssfzo12bi  13665  elfznelfzo  13677  modaddmodup  13845  modfzo0difsn  13854  fsuppmapnn0fiubex  13903  seqf1o  13954  expcllem  13983  expeq0  14003  mulexp  14012  hashgt12el2  14334  hashimarni  14352  hash2prd  14386  fi1uzind  14418  swrdnd  14566  swrdswrdlem  14615  swrdswrd  14616  pfxccat3  14645  reuccatpfxs1  14658  repswswrd  14695  repswccat  14697  cshwidxmod  14714  2cshwcshw  14736  s4f1o  14829  wwlktovfo  14869  relexpindlem  14974  resqrex  15161  summo  15628  fsum2d  15682  modfsummods  15704  binom  15741  clim2prod  15799  fprod2d  15892  binomfallfac  15952  efexp  16014  demoivreALT  16114  divconjdvds  16230  addmodlteqALT  16240  dfgcd2  16461  lcmfunsnlem2lem1  16553  lcmfdvdsb  16558  lcmfun  16560  coprmprod  16576  coprmproddvdslem  16577  oddprmdvds  16819  ramcl  16945  prmgaplem6  16972  cshwsidrepswmod0  17010  cshwshashlem1  17011  cshwshashlem2  17012  ressress  17162  initoeu2lem1  17925  symggen  19386  pmtr3ncom  19391  gsumle  20061  srgmulgass  20139  srgbinom  20153  ringinvnzdiv  20223  rhmsubcrngclem2  20586  lmodvsmmulgdi  20834  nzerooringczr  21421  ofldchr  21517  psgndiflemB  21541  assamulgscmlem2  21841  mptcoe1fsupp  22131  coe1fzgsumdlem  22221  evl1gsumdlem  22274  scmatmulcl  22436  mdetdiagid  22518  pm2mpf1  22717  mptcoe1matfsupp  22720  mp2pm2mplem4  22727  chpdmat  22759  chfacfisf  22772  chfacfisfcpmat  22773  chcoeffeq  22804  topbas  22890  elcls  22991  elcls3  23001  2ndcdisj  23374  filufint  23838  ovoliunlem3  25435  dvge0  25941  ulmcn  26338  gausslemma2dlem3  27309  nosupbnd1  27656  nosupbnd2  27658  noinfbnd1  27671  noinfbnd2  27673  sizusglecusg  29446  upgriswlk  29623  2pthnloop  29713  crctcshwlkn0  29803  wlknwwlksnbij  29870  wwlksnred  29874  wwlksnext  29875  wwlksnextinj  29881  wwlksnextproplem2  29892  wwlksnextproplem3  29893  usgr2wspthons3  29949  clwwlkccatlem  29973  clwlkclwwlklem2a4  29981  clwlkclwwlklem2a  29982  clwlkclwwlklem2  29984  erclwwlktr  30006  clwwlkinwwlk  30024  clwwlkf  30031  clwwlkf1  30033  wwlksext2clwwlk  30041  clwwlknscsh  30046  umgr2cwwk2dif  30048  erclwwlkntr  30055  clwwlknonex2  30093  uhgr3cyclex  30166  upgr4cycl4dv4e  30169  eucrctshift  30227  3cyclfrgrrn1  30269  frgrwopreglem2  30297  frgrwopreglem5  30305  frgrwopreglem5ALT  30306  numclwwlk1lem2fo  30342  numclwlk2lem2f  30361  numclwlk2lem2f1o  30363  frgrreg  30378  friendshipgt3  30382  friendship  30383  ipasslem1  30815  shmodsi  31373  elspansn5  31558  h1datomi  31565  nmopsetretALT  31847  pjss2coi  32148  pj3cor1i  32193  mdexchi  32319  atcvat4i  32381  mdsymlem3  32389  mdsymlem4  32390  sumdmdii  32399  cdj3lem2b  32421  elabreximd  32494  iuninc  32544  iundisjf  32573  xrsmulgzz  32999  gsumvsca1  33204  gsumvsca2  33205  unitprodclb  33363  rprmdvdsprod  33508  1arithidom  33511  constrmon  33780  locfinreflem  33876  xrge0iifiso  33971  lmxrge0  33988  esumfzf  34105  sigaclfu2  34157  signstfvneq0  34608  satfrel  35434  satfrnmapom  35437  fmlafvel  35452  fmlasuc  35453  bccolsum  35806  faclimlem1  35810  segletr  36181  segleantisym  36182  outsideoftr  36196  exp5d  36369  elicc3  36384  finxpreclem2  37457  wl-sbcom2d  37628  poimirlem26  37709  mblfinlem3  37722  itg2addnc  37737  indexa  37796  disjlem19  38922  ax12indalem  39067  ax12inda2ALT  39068  cvrat4  39565  elpaddn0  39922  paddasslem5  39946  paddasslem14  39955  eldioph2  42882  pell1234qrdich  42981  oaabsb  43414  onmcl  43451  tfsconcat0b  43466  oaun3lem1  43494  oaun3lem2  43495  naddgeoa  43514  gneispb  44251  rexlimd3  45268  rexabslelem  45543  climsuselem1  45734  stoweidlem19  46144  stoweidlem20  46145  stoweidlem34  46159  wallispilem3  46192  sge0iunmpt  46543  meaiuninc3v  46609  smflimmpt  46935  or2expropbilem1  47159  fsetprcnexALT  47189  2reu8i  47240  2elfz2melfz  47445  subsubelfzo0  47453  iccpartigtl  47550  iccpartgt  47554  icceuelpartlem  47562  fargshiftf1  47568  ich2exprop  47598  ichreuopeq  47600  lighneallem3  47734  gbowgt5  47889  bgoldbtbndlem3  47934  bgoldbtbndlem4  47935  bgoldbtbnd  47936  tgblthelfgott  47942  grimco  48016  isuspgrimlem  48022  grimedg  48062  upgrwlkupwlk  48267  2zrngagrp  48376  lmodvsmdi  48506  ply1mulgsumlem1  48514  elfzolborelfzop1  48647  nnolog2flm1  48718  nn0sumshdiglemA  48747  eenglngeehlnmlem2  48866