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  3143  r19.29af2  3250  reusv2lem2  5369  pwssun  5545  onmindif  6446  mpteqb  7005  dffo3f  7096  fompt  7108  fliftfun  7305  elovmpt3rab1  7667  ordsucss  7812  tfindsg  7856  tfrlem1  8390  tfrlem9  8399  oaordi  8558  oaordex  8570  oaass  8573  oarec  8574  omass  8592  oen0  8598  oeordsuc  8606  nnaordi  8630  omsmolem  8669  naddssim  8697  brinxper  8748  infensuc  9169  php3OLD  9233  suppeqfsuppbi  9391  marypha1lem  9445  hartogs  9558  card2on  9568  tz9.12lem3  9803  infxpenlem  10027  cfcoflem  10286  isf32lem12  10378  zorn2lem6  10515  ondomon  10577  axrepnd  10608  fpwwe2lem11  10655  genpcd  11020  ltexprlem6  11055  axpre-sup  11183  negf1o  11667  recex  11869  uzaddcl  12920  nn01to3  12957  rpnnen1lem5  12997  xrsupsslem  13323  xrinfmsslem  13324  supxrunb1  13335  supxrunb2  13336  fz0fzelfz0  13651  fz0fzdiffz0  13654  elfzmlbp  13656  difelfzle  13658  fzo1fzo0n0  13731  elincfzoext  13739  ssfzo12bi  13777  elfznelfzo  13788  modaddmodup  13952  modfzo0difsn  13961  fsuppmapnn0fiubex  14010  seqf1o  14061  expcllem  14090  expeq0  14110  mulexp  14119  hashgt12el2  14441  hashimarni  14459  hash2prd  14493  fi1uzind  14525  swrdnd  14672  swrdswrdlem  14722  swrdswrd  14723  pfxccat3  14752  reuccatpfxs1  14765  repswswrd  14802  repswccat  14804  cshwidxmod  14821  2cshwcshw  14844  s4f1o  14937  wwlktovfo  14977  relexpindlem  15082  resqrex  15269  summo  15733  fsum2d  15787  modfsummods  15809  binom  15846  clim2prod  15904  fprod2d  15997  binomfallfac  16057  efexp  16119  demoivreALT  16219  divconjdvds  16334  addmodlteqALT  16344  dfgcd2  16565  lcmfunsnlem2lem1  16657  lcmfdvdsb  16662  lcmfun  16664  coprmprod  16680  coprmproddvdslem  16681  oddprmdvds  16923  ramcl  17049  prmgaplem6  17076  cshwsidrepswmod0  17114  cshwshashlem1  17115  cshwshashlem2  17116  ressress  17268  initoeu2lem1  18027  symggen  19451  pmtr3ncom  19456  srgmulgass  20177  srgbinom  20191  ringinvnzdiv  20261  rhmsubcrngclem2  20627  lmodvsmmulgdi  20854  nzerooringczr  21441  psgndiflemB  21560  assamulgscmlem2  21860  mptcoe1fsupp  22151  coe1fzgsumdlem  22241  evl1gsumdlem  22294  scmatmulcl  22456  mdetdiagid  22538  pm2mpf1  22737  mptcoe1matfsupp  22740  mp2pm2mplem4  22747  chpdmat  22779  chfacfisf  22792  chfacfisfcpmat  22793  chcoeffeq  22824  topbas  22910  elcls  23011  elcls3  23021  2ndcdisj  23394  filufint  23858  ovoliunlem3  25457  dvge0  25963  ulmcn  26360  gausslemma2dlem3  27331  nosupbnd1  27678  nosupbnd2  27680  noinfbnd1  27693  noinfbnd2  27695  sizusglecusg  29443  upgriswlk  29621  2pthnloop  29713  crctcshwlkn0  29803  wlknwwlksnbij  29870  wwlksnred  29874  wwlksnext  29875  wwlksnextinj  29881  wwlksnextproplem2  29892  wwlksnextproplem3  29893  usgr2wspthons3  29946  clwwlkccatlem  29970  clwlkclwwlklem2a4  29978  clwlkclwwlklem2a  29979  clwlkclwwlklem2  29981  erclwwlktr  30003  clwwlkinwwlk  30021  clwwlkf  30028  clwwlkf1  30030  wwlksext2clwwlk  30038  clwwlknscsh  30043  umgr2cwwk2dif  30045  erclwwlkntr  30052  clwwlknonex2  30090  uhgr3cyclex  30163  upgr4cycl4dv4e  30166  eucrctshift  30224  3cyclfrgrrn1  30266  frgrwopreglem2  30294  frgrwopreglem5  30302  frgrwopreglem5ALT  30303  numclwwlk1lem2fo  30339  numclwlk2lem2f  30358  numclwlk2lem2f1o  30360  frgrreg  30375  friendshipgt3  30379  friendship  30380  ipasslem1  30812  shmodsi  31370  elspansn5  31555  h1datomi  31562  nmopsetretALT  31844  pjss2coi  32145  pj3cor1i  32190  mdexchi  32316  atcvat4i  32378  mdsymlem3  32386  mdsymlem4  32387  sumdmdii  32396  cdj3lem2b  32418  elabreximd  32491  iuninc  32541  iundisjf  32570  xrsmulgzz  33001  gsumle  33092  gsumvsca1  33223  gsumvsca2  33224  ofldchr  33336  unitprodclb  33404  rprmdvdsprod  33549  1arithidom  33552  constrmon  33778  locfinreflem  33871  xrge0iifiso  33966  lmxrge0  33983  esumfzf  34100  sigaclfu2  34152  signstfvneq0  34604  satfrel  35389  satfrnmapom  35392  fmlafvel  35407  fmlasuc  35408  bccolsum  35756  faclimlem1  35760  segletr  36132  segleantisym  36133  outsideoftr  36147  exp5d  36320  elicc3  36335  finxpreclem2  37408  wl-sbcom2d  37579  poimirlem26  37670  mblfinlem3  37683  itg2addnc  37698  indexa  37757  disjlem19  38819  ax12indalem  38963  ax12inda2ALT  38964  cvrat4  39462  elpaddn0  39819  paddasslem5  39843  paddasslem14  39852  eldioph2  42785  pell1234qrdich  42884  oaabsb  43318  onmcl  43355  tfsconcat0b  43370  oaun3lem1  43398  oaun3lem2  43399  naddgeoa  43418  gneispb  44155  rexlimd3  45168  rexabslelem  45445  climsuselem1  45636  stoweidlem19  46048  stoweidlem20  46049  stoweidlem34  46063  wallispilem3  46096  sge0iunmpt  46447  meaiuninc3v  46513  smflimmpt  46839  or2expropbilem1  47061  fsetprcnexALT  47091  2reu8i  47142  2elfz2melfz  47347  subsubelfzo0  47355  iccpartigtl  47437  iccpartgt  47441  icceuelpartlem  47449  fargshiftf1  47455  ich2exprop  47485  ichreuopeq  47487  lighneallem3  47621  gbowgt5  47776  bgoldbtbndlem3  47821  bgoldbtbndlem4  47822  bgoldbtbnd  47823  tgblthelfgott  47829  grimco  47902  isuspgrimlem  47908  grimedg  47948  upgrwlkupwlk  48115  2zrngagrp  48224  lmodvsmdi  48354  ply1mulgsumlem1  48362  elfzolborelfzop1  48495  nnolog2flm1  48570  nn0sumshdiglemA  48599  eenglngeehlnmlem2  48718