Theorem exp31 425

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  exp41  440  exp42  441  imp5a  446  expl  463  anasss  472  an31s  667  exbiri  823  3exp  1137  exp516  1375  rexlimdva2  3165  r19.29af2  3270  reusv2lem2  5360  pwssun  5542  onmindif  6457  mpteqb  7014  dffo3f  7107  fompt  7119  fliftfun  7321  elovmpt3rab1  7682  ordsucss  7830  tfindsg  7873  tfrlem1  8387  tfrlem9  8397  oaordi  8558  oaordex  8570  oaass  8573  oarec  8574  omass  8592  oen0  8599  oeordsuc  8607  nnaordi  8631  omsmolem  8670  naddssim  8699  brinxper  8751  infensuc  9178  suppeqfsuppbi  9375  marypha1lem  9429  hartogs  9542  card2on  9552  tz9.12lem3  9800  infxpenlem  10096  cfcoflem  10354  isf32lem12  10446  zorn2lem6  10583  ondomon  10651  axrepnd  10683  fpwwe2lem11  10730  genpcd  11095  ltexprlem6  11130  axpre-sup  11258  negf1o  11750  recex  11952  uzaddcl  13035  nn01to3  13072  rpnnen1lem5  13113  xrsupsslem  13441  xrinfmsslem  13442  supxrunb1  13453  supxrunb2  13454  fz0fzelfz0  13772  fz0fzdiffz0  13775  elfzmlbp  13777  difelfzle  13779  fzo1fzo0n0  13854  elincfzoext  13862  ssfzo12bi  13900  elfznelfzo  13912  modaddmodup  14081  modfzo0difsn  14090  fsuppmapnn0fiubex  14139  seqf1o  14190  expcllem  14219  expeq0  14239  mulexp  14248  hashgt12el2  14572  hashimarni  14590  hash2prd  14624  fi1uzind  14656  swrdnd  14809  swrdswrdlem  14858  swrdswrd  14859  pfxccat3  14888  reuccatpfxs1  14901  repswswrd  14940  repswccat  14942  cshwidxmod  14959  2cshwcshw  14981  s4f1o  15075  wwlktovfo  15117  relexpindlem  15222  resqrex  15423  summo  15889  fsum2d  15943  modfsummods  15966  binom  16005  clim2prod  16063  fprod2d  16154  binomfallfac  16213  efexp  16275  demoivreALT  16375  divconjdvds  16491  addmodlteqALT  16501  dfgcd2  16725  lcmfunsnlem2lem1  16819  lcmfdvdsb  16824  lcmfun  16826  coprmprod  16842  coprmproddvdslem  16843  oddprmdvds  17087  ramcl  17213  prmgaplem6  17240  cshwsidrepswmod0  17278  cshwshashlem1  17279  cshwshashlem2  17280  ressress  17431  initoeu2lem1  18195  mgmn0plusgplusf  18834  symggen  19690  pmtr3ncom  19695  gsumle  20365  srgmulgass  20449  srgbinom  20463  ringinvnzdiv  20538  rhmsubcrngclem2  20925  lmodvsmmulgdi  21178  nzerooringczr  21792  ofldchr  21888  psgndiflemB  21912  assamulgscmlem2  22214  mptcoe1fsupp  22539  coe1fzgsumdlem  22627  evl1gsumdlem  22680  scmatmulcl  22839  mdetdiagid  22921  pm2mpf1  23123  mptcoe1matfsupp  23126  mp2pm2mplem4  23133  chpdmat  23165  chfacfisf  23178  chfacfisfcpmat  23179  chcoeffeq  23210  topbas  23296  elcls  23397  elcls3  23407  2ndcdisj  23781  filufint  24245  ovoliunlem3  25831  dvge0  26332  ulmcn  26732  gausslemma2dlem3  27701  nosupbnd1  28077  nosupbnd2  28079  noinfbnd1  28092  noinfbnd2  28094  sizusglecusg  30050  upgriswlk  30227  2pthnloop  30323  crctcshwlkn0  30416  wlknwwlksnbij  30483  wwlksnred  30487  wwlksnext  30488  wwlksnextinj  30494  wwlksnextproplem2  30505  wwlksnextproplem3  30506  usgr2wspthons3  30562  clwwlkccatlem  30586  clwlkclwwlklem2a4  30594  clwlkclwwlklem2a  30595  clwlkclwwlklem2  30597  erclwwlktr  30619  clwwlkinwwlk  30637  clwwlkf  30644  clwwlkf1  30646  wwlksext2clwwlk  30654  clwwlknscsh  30659  umgr2cwwk2dif  30661  erclwwlkntr  30668  clwwlknonex2  30706  uhgr3cyclex  30789  upgr4cycl4dv4e  30792  eucrctshift  30850  3cyclfrgrrn1  30892  frgrwopreglem2  30920  frgrwopreglem5  30928  frgrwopreglem5ALT  30929  numclwwlk1lem2fo  30965  numclwlk2lem2f  30984  numclwlk2lem2f1o  30986  frgrreg  31001  friendshipgt3  31005  friendship  31006  ipasslem1  31439  shmodsi  31997  elspansn5  32182  h1datomi  32189  nmopsetretALT  32471  pjss2coi  32772  pj3cor1i  32817  mdexchi  32943  atcvat4i  33005  mdsymlem3  33013  mdsymlem4  33014  sumdmdii  33023  cdj3lem2b  33045  elabreximd  33154  iuninc  33203  iundisjf  33231  acunirnmpt2  33302  acunirnmpt2f  33303  xrsmulgzz  33617  gsumvsca1  33834  gsumvsca2  33835  unitprodclb  33991  rprmdvdsprod  34113  1arithidom  34116  constrmon  34423  locfinreflem  34519  xrge0iifiso  34614  lmxrge0  34631  esumfzf  34748  sigaclfu2  34800  signstfvneq0  35248  satfrel  36219  satfrnmapom  36222  fmlafvel  36237  fmlasuc  36238  bccolsum  36597  faclimlem1  36601  segletr  36972  segleantisym  36973  outsideoftr  36987  exp5d  37184  elicc3  37198  mh-inf3f1  37422  finxpreclem2  38407  wl-sbcom2d  38587  poimirlem26  38658  mblfinlem3  38671  itg2addnc  38686  indexa  38761  disjlem19  39930  ax12indalem  40096  ax12inda2ALT  40097  cvrat4  40594  elpaddn0  40951  paddasslem5  40975  paddasslem14  40984  eldioph2  43867  pell1234qrdich  43962  oaabsb  44390  onmcl  44427  tfsconcat0b  44442  oaun3lem1  44470  oaun3lem2  44471  naddgeoa  44490  gneispb  45225  rexlimd3  46253  rexabslelem  46522  climsuselem1  46713  stoweidlem19  47123  stoweidlem20  47124  stoweidlem34  47138  wallispilem3  47171  sge0iunmpt  47522  meaiuninc3v  47588  smflimmpt  47914  or2expropbilem1  48196  fsetprcnexALT  48226  2reu8i  48277  2elfz2melfz  48482  subsubelfzo0  48491  iccpartigtl  48599  iccpartgt  48603  icceuelpartlem  48611  fargshiftf1  48617  ich2exprop  48647  ichreuopeq  48649  lighneallem3  48786  gbowgt5  48954  bgoldbtbndlem3  48999  bgoldbtbndlem4  49000  bgoldbtbnd  49001  tgblthelfgott  49007  grimco  49081  isuspgrimlem  49087  grimedg  49127  upgrwlkupwlk  49332  2zrngagrp  49440  lmodvsmdi  49585  ply1mulgsumlem1  49592  elfzolborelfzop1  49725  nnolog2flm1  49796  nn0sumshdiglemA  49825  eenglngeehlnmlem2  49945