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

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

Proof of Theorem simprlr
StepHypRef Expression
1 simpr 476 . 2 ((𝜓𝜒) → 𝜒)
21ad2antrl 764 1 ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  disjxiunOLD  4682  fcof1  6582  fliftfun  6602  wfrlem17  7476  domunfican  8274  finsschain  8314  suppeqfsuppbi  8330  fsuppunbi  8337  wemapsolem  8496  wemapso  8497  wemapso2lem  8498  cantnf  8628  enfin2i  9181  ttukeylem7  9375  fpwwe2lem2  9492  fpwwe2lem9  9498  fpwwe2lem12  9501  fpwwelem  9505  distrlem4pr  9886  mulcmpblnr  9930  prsrlem1  9931  addsrmo  9932  mulsrmo  9933  divdivdiv  10764  divsubdiv  10779  lediv12a  10954  xmullem  12132  xlemul1a  12156  seqcaopr  12878  leexp2r  12958  hashf1lem1  13277  hashf1lem2  13278  fi1uzind  13317  brfi1indALT  13320  wrd2ind  13523  cshweqrep  13613  summolem2  14491  summo  14492  prodmolem2  14709  prodmo  14710  bezoutlem3  15305  bezoutlem4  15306  qredeu  15419  pcadd  15640  vdwlem9  15740  vdwlem10  15741  ramub1lem2  15778  ramub1  15779  cofucl  16595  setcmon  16784  poslubmo  17193  posglbmo  17194  grprcan  17502  isnsg3  17675  ghmpreima  17729  gaorber  17787  psgneu  17972  odcau  18065  lsmsubm  18114  lsmmod  18134  efgsfo  18198  ablfaclem3  18532  ringpropd  18628  islmodd  18917  lmodprop2d  18973  lss1d  19011  assamulgscmlem2  19397  mplcoe1  19513  mplcoe5  19516  evlslem1  19563  lindff1  20207  islindf4  20225  mdetunilem7  20472  mdetunilem8  20473  mdetunilem9  20474  mdetuni0  20475  mdetmul  20477  ppttop  20859  epttop  20861  cnhaus  21206  isreg2  21229  cncmp  21243  1stcfb  21296  2ndcomap  21309  cldllycmp  21346  txcls  21455  ptclsg  21466  ptcnp  21473  txdis1cn  21486  txlly  21487  txnlly  21488  pthaus  21489  txhaus  21498  txkgen  21503  xkohaus  21504  xkococnlem  21510  xkococn  21511  fgabs  21730  rnelfm  21804  hausflimi  21831  hausflim  21832  alexsubALTlem2  21899  alexsubALTlem4  21901  alexsubALT  21902  tgpconncomp  21963  qustgplem  21971  metequiv2  22362  met2ndci  22374  nrmmetd  22426  nlmvscnlem1  22537  reconn  22678  xrge0tsms  22684  ipcnlem1  23090  minveclem3  23246  pmltpc  23265  ovolicc2lem5  23335  ovolicc2  23336  uniioombllem6  23402  dyadmbllem  23413  vitalilem3  23424  mbfmullem  23537  itg2split  23561  itg2mono  23565  dvlip2  23803  lhop1  23822  dvcnvrelem1  23825  ftc1lem6  23849  itgsubst  23857  dgrco  24076  plyexmo  24113  ulmdvlem3  24201  abelthlem2  24231  abelthlem8  24238  dvdsmulf1o  24965  chpchtsum  24989  dchrptlem2  25035  2sqlem5  25192  2sqlem9  25197  2sqb  25202  pntrlog2bnd  25318  pntibndlem3  25326  pntlemp  25344  pnt3  25346  hlcgreu  25558  mirreu3  25594  cgraswap  25757  cgracom  25759  cgratr  25760  acopyeu  25770  axsegcon  25852  ax5seglem9  25862  axeuclid  25888  axcontlem12  25900  clwwlkf1  27012  wwlksext2clwwlkOLD  27022  frgrnbnb  27273  ablo4  27532  smcnlem  27680  pjhthmo  28289  pjpjpre  28406  3oalem2  28650  lnconi  29020  atom1d  29340  resf1o  29633  xrge0tsmsd  29913  ballotlemfc0  30682  ballotlemfcc  30683  pconnconn  31339  cvmfolem  31387  cvmliftmo  31392  cvmliftlem7  31399  cvmlift2lem10  31420  cvmlift3lem8  31434  noresle  31971  lineext  32308  linecgr  32313  btwnconn1lem10  32328  btwnconn1lem11  32329  btwnconn3  32335  brsegle  32340  seglecgr12im  32342  segleantisym  32347  outsideoftr  32361  outsideofeq  32362  outsideofeu  32363  linethru  32385  finminlem  32437  neibastop2lem  32480  isbasisrelowllem1  33333  isbasisrelowllem2  33334  mblfinlem3  33578  bddiblnc  33610  ftc1cnnc  33614  isbnd3  33713  heibor1lem  33738  crngm4  33932  cvlcvr1  34944  4atlem12  35216  paddasslem12  35435  paddasslem13  35436  lhpexle2lem  35613  trlord  36174  cdlemkid4  36539  dihopelvalcpre  36854  dihmeetlem1N  36896  dihglblem5apreN  36897  dihmeetlem6  36915  dih1dimatlem0  36934  dihjatcclem4  37027  mzpcl2  37610  mzpmfp  37627  mzpcompact2lem  37631  diophin  37653  pell14qrmulcl  37744  hbtlem2  38011  iunrelexpuztr  38328  stoweidlem61  40596  fourierdlem92  40733  snlindsntor  42585  elfzolborelfzop1  42634  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator