MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simprlr Structured version   Visualization version   GIF version

Theorem simprlr 779
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprlr ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜒)

Proof of Theorem simprlr
StepHypRef Expression
1 simpr 486 . 2 ((𝜓𝜒) → 𝜒)
21ad2antrl 727 1 ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  fcof1  7234  fliftfun  7258  fprresex  8242  wfrlem17OLD  8272  domunfican  9267  finsschain  9306  suppeqfsuppbi  9324  fsuppunbi  9331  wemapsolem  9491  wemapso  9492  wemapso2lem  9493  cantnf  9634  enfin2i  10262  ttukeylem7  10456  fpwwe2lem2  10573  fpwwe2lem8  10579  fpwwe2lem11  10582  fpwwelem  10586  distrlem4pr  10967  mulcmpblnr  11012  prsrlem1  11013  addsrmo  11014  mulsrmo  11015  divdivdiv  11861  divsubdiv  11876  lediv12a  12053  xmullem  13189  xlemul1a  13213  seqcaopr  13951  leexp2r  14085  hashf1lem1  14359  hashf1lem1OLD  14360  hashf1lem2  14361  fi1uzind  14402  brfi1indALT  14405  wrd2ind  14617  swrdccat  14629  cshweqrep  14715  rtrclreclem4  14952  summolem2  15606  summo  15607  prodmolem2  15823  prodmo  15824  bezoutlem3  16427  bezoutlem4  16428  qredeu  16539  pcadd  16766  vdwlem9  16866  vdwlem10  16867  ramub1lem2  16904  ramub1  16905  cofucl  17779  setcmon  17978  poslubmo  18305  posglbmo  18306  grprcan  18789  isnsg3  18967  ghmpreima  19035  gaorber  19093  psgneu  19293  odcau  19391  lsmsubm  19440  lsmmod  19462  efgsfo  19526  ablfaclem3  19871  ringpropd  20011  islmodd  20342  lmodprop2d  20399  lss1d  20439  lindff1  21242  islindf4  21260  assamulgscmlem2  21319  mplcoe1  21454  mplcoe5  21457  evlslem1  21508  mdetunilem7  21983  mdetunilem8  21984  mdetunilem9  21985  mdetuni0  21986  mdetmul  21988  ppttop  22373  epttop  22375  cnhaus  22721  isreg2  22744  cncmp  22759  1stcfb  22812  2ndcomap  22825  cldllycmp  22862  txcls  22971  ptclsg  22982  ptcnp  22989  txdis1cn  23002  txlly  23003  txnlly  23004  pthaus  23005  txhaus  23014  txkgen  23019  xkohaus  23020  xkococnlem  23026  xkococn  23027  fgabs  23246  rnelfm  23320  hausflimi  23347  hausflim  23348  alexsubALTlem2  23415  alexsubALTlem4  23417  alexsubALT  23418  tgpconncomp  23480  qustgplem  23488  metequiv2  23882  met2ndci  23894  nrmmetd  23946  nlmvscnlem1  24066  reconn  24207  xrge0tsms  24213  ipcnlem1  24625  minveclem3  24809  pmltpc  24830  ovolicc2lem5  24901  ovolicc2  24902  uniioombllem6  24968  dyadmbllem  24979  vitalilem3  24990  mbfmullem  25106  itg2split  25130  itg2mono  25134  bddiblnc  25222  dvlip2  25375  lhop1  25394  dvcnvrelem1  25397  ftc1lem6  25421  itgsubst  25429  dgrco  25652  plyexmo  25689  ulmdvlem3  25777  abelthlem2  25807  abelthlem8  25814  dvdsmulf1o  26559  chpchtsum  26583  dchrptlem2  26629  2sqlem5  26786  2sqlem9  26791  2sqb  26796  pntrlog2bnd  26948  pntibndlem3  26956  pntlemp  26974  pnt3  26976  noresle  27061  nosupprefixmo  27064  noinfprefixmo  27065  addsprop  27310  tgjustf  27457  hlcgreu  27602  mirreu3  27638  cgraswap  27804  cgracom  27806  cgratr  27807  flatcgra  27808  acopyeu  27818  axsegcon  27918  ax5seglem9  27928  axeuclid  27954  axcontlem12  27966  clwwlkf1  29035  n4cyclfrgr  29277  frgrnbnb  29279  ablo4  29534  smcnlem  29681  pjhthmo  30286  pjpjpre  30403  3oalem2  30647  lnconi  31017  atom1d  31337  resf1o  31694  mgcoval  31895  xrge0tsmsd  31948  ballotlemfc0  33149  ballotlemfcc  33150  pconnconn  33882  cvmfolem  33930  cvmliftmo  33935  cvmliftlem7  33942  cvmlift2lem10  33963  cvmlift3lem8  33977  lineext  34707  linecgr  34712  btwnconn1lem10  34727  btwnconn1lem11  34728  btwnconn3  34734  brsegle  34739  seglecgr12im  34741  segleantisym  34746  outsideoftr  34760  outsideofeq  34761  outsideofeu  34762  linethru  34784  finminlem  34836  neibastop2lem  34878  isbasisrelowllem1  35872  isbasisrelowllem2  35873  mblfinlem3  36163  ftc1cnnc  36196  isbnd3  36289  heibor1lem  36314  crngm4  36508  cvlcvr1  37847  4atlem12  38121  paddasslem12  38340  paddasslem13  38341  lhpexle2lem  38518  trlord  39078  cdlemkid4  39443  dihopelvalcpre  39757  dihmeetlem1N  39799  dihglblem5apreN  39800  dihmeetlem6  39818  dih1dimatlem0  39837  dihjatcclem4  39930  prjspner1  41007  mzpcl2  41096  mzpmfp  41113  mzpcompact2lem  41117  diophin  41138  pell14qrmulcl  41229  hbtlem2  41494  iunrelexpuztr  42079  stoweidlem61  44388  fourierdlem92  44525  euoreqb  45427  prproropf1olem3  45783  prproropf1olem4  45784  fpprwpprb  46018  snlindsntor  46638  elfzolborelfzop1  46686  nn0sumshdiglemB  46792
  Copyright terms: Public domain W3C validator