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  3135  r19.29af2  3240  reusv2lem2  5337  pwssun  5508  onmindif  6400  mpteqb  6948  dffo3f  7039  fompt  7051  fliftfun  7246  elovmpt3rab1  7606  ordsucss  7748  tfindsg  7791  tfrlem1  8295  tfrlem9  8304  oaordi  8461  oaordex  8473  oaass  8476  oarec  8477  omass  8495  oen0  8501  oeordsuc  8509  nnaordi  8533  omsmolem  8572  naddssim  8600  brinxper  8651  infensuc  9068  suppeqfsuppbi  9263  marypha1lem  9317  hartogs  9430  card2on  9440  tz9.12lem3  9682  infxpenlem  9904  cfcoflem  10163  isf32lem12  10255  zorn2lem6  10392  ondomon  10454  axrepnd  10485  fpwwe2lem11  10532  genpcd  10897  ltexprlem6  10932  axpre-sup  11060  negf1o  11547  recex  11749  uzaddcl  12802  nn01to3  12839  rpnnen1lem5  12879  xrsupsslem  13206  xrinfmsslem  13207  supxrunb1  13218  supxrunb2  13219  fz0fzelfz0  13534  fz0fzdiffz0  13537  elfzmlbp  13539  difelfzle  13541  fzo1fzo0n0  13615  elincfzoext  13623  ssfzo12bi  13661  elfznelfzo  13673  modaddmodup  13841  modfzo0difsn  13850  fsuppmapnn0fiubex  13899  seqf1o  13950  expcllem  13979  expeq0  13999  mulexp  14008  hashgt12el2  14330  hashimarni  14348  hash2prd  14382  fi1uzind  14414  swrdnd  14562  swrdswrdlem  14611  swrdswrd  14612  pfxccat3  14641  reuccatpfxs1  14654  repswswrd  14691  repswccat  14693  cshwidxmod  14710  2cshwcshw  14732  s4f1o  14825  wwlktovfo  14865  relexpindlem  14970  resqrex  15157  summo  15624  fsum2d  15678  modfsummods  15700  binom  15737  clim2prod  15795  fprod2d  15888  binomfallfac  15948  efexp  16010  demoivreALT  16110  divconjdvds  16226  addmodlteqALT  16236  dfgcd2  16457  lcmfunsnlem2lem1  16549  lcmfdvdsb  16554  lcmfun  16556  coprmprod  16572  coprmproddvdslem  16573  oddprmdvds  16815  ramcl  16941  prmgaplem6  16968  cshwsidrepswmod0  17006  cshwshashlem1  17007  cshwshashlem2  17008  ressress  17158  initoeu2lem1  17921  symggen  19383  pmtr3ncom  19388  gsumle  20058  srgmulgass  20136  srgbinom  20150  ringinvnzdiv  20220  rhmsubcrngclem2  20583  lmodvsmmulgdi  20831  nzerooringczr  21418  ofldchr  21514  psgndiflemB  21538  assamulgscmlem2  21838  mptcoe1fsupp  22129  coe1fzgsumdlem  22219  evl1gsumdlem  22272  scmatmulcl  22434  mdetdiagid  22516  pm2mpf1  22715  mptcoe1matfsupp  22718  mp2pm2mplem4  22725  chpdmat  22757  chfacfisf  22770  chfacfisfcpmat  22771  chcoeffeq  22802  topbas  22888  elcls  22989  elcls3  22999  2ndcdisj  23372  filufint  23836  ovoliunlem3  25433  dvge0  25939  ulmcn  26336  gausslemma2dlem3  27307  nosupbnd1  27654  nosupbnd2  27656  noinfbnd1  27669  noinfbnd2  27671  sizusglecusg  29443  upgriswlk  29620  2pthnloop  29710  crctcshwlkn0  29800  wlknwwlksnbij  29867  wwlksnred  29871  wwlksnext  29872  wwlksnextinj  29878  wwlksnextproplem2  29889  wwlksnextproplem3  29890  usgr2wspthons3  29943  clwwlkccatlem  29967  clwlkclwwlklem2a4  29975  clwlkclwwlklem2a  29976  clwlkclwwlklem2  29978  erclwwlktr  30000  clwwlkinwwlk  30018  clwwlkf  30025  clwwlkf1  30027  wwlksext2clwwlk  30035  clwwlknscsh  30040  umgr2cwwk2dif  30042  erclwwlkntr  30049  clwwlknonex2  30087  uhgr3cyclex  30160  upgr4cycl4dv4e  30163  eucrctshift  30221  3cyclfrgrrn1  30263  frgrwopreglem2  30291  frgrwopreglem5  30299  frgrwopreglem5ALT  30300  numclwwlk1lem2fo  30336  numclwlk2lem2f  30355  numclwlk2lem2f1o  30357  frgrreg  30372  friendshipgt3  30376  friendship  30377  ipasslem1  30809  shmodsi  31367  elspansn5  31552  h1datomi  31559  nmopsetretALT  31841  pjss2coi  32142  pj3cor1i  32187  mdexchi  32313  atcvat4i  32375  mdsymlem3  32383  mdsymlem4  32384  sumdmdii  32393  cdj3lem2b  32415  elabreximd  32488  iuninc  32538  iundisjf  32567  xrsmulgzz  32988  gsumvsca1  33193  gsumvsca2  33194  unitprodclb  33352  rprmdvdsprod  33497  1arithidom  33500  constrmon  33755  locfinreflem  33851  xrge0iifiso  33946  lmxrge0  33963  esumfzf  34080  sigaclfu2  34132  signstfvneq0  34583  satfrel  35409  satfrnmapom  35412  fmlafvel  35427  fmlasuc  35428  bccolsum  35781  faclimlem1  35785  segletr  36154  segleantisym  36155  outsideoftr  36169  exp5d  36342  elicc3  36357  finxpreclem2  37430  wl-sbcom2d  37601  poimirlem26  37692  mblfinlem3  37705  itg2addnc  37720  indexa  37779  disjlem19  38845  ax12indalem  38990  ax12inda2ALT  38991  cvrat4  39488  elpaddn0  39845  paddasslem5  39869  paddasslem14  39878  eldioph2  42801  pell1234qrdich  42900  oaabsb  43333  onmcl  43370  tfsconcat0b  43385  oaun3lem1  43413  oaun3lem2  43414  naddgeoa  43433  gneispb  44170  rexlimd3  45187  rexabslelem  45462  climsuselem1  45653  stoweidlem19  46063  stoweidlem20  46064  stoweidlem34  46078  wallispilem3  46111  sge0iunmpt  46462  meaiuninc3v  46528  smflimmpt  46854  or2expropbilem1  47069  fsetprcnexALT  47099  2reu8i  47150  2elfz2melfz  47355  subsubelfzo0  47363  iccpartigtl  47460  iccpartgt  47464  icceuelpartlem  47472  fargshiftf1  47478  ich2exprop  47508  ichreuopeq  47510  lighneallem3  47644  gbowgt5  47799  bgoldbtbndlem3  47844  bgoldbtbndlem4  47845  bgoldbtbnd  47846  tgblthelfgott  47852  grimco  47926  isuspgrimlem  47932  grimedg  47972  upgrwlkupwlk  48177  2zrngagrp  48286  lmodvsmdi  48416  ply1mulgsumlem1  48424  elfzolborelfzop1  48557  nnolog2flm1  48628  nn0sumshdiglemA  48657  eenglngeehlnmlem2  48776