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

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

Proof of Theorem simprlr
StepHypRef Expression
1 simpr 485 . 2 ((𝜓𝜒) → 𝜒)
21ad2antrl 724 1 ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  fcof1  7039  fliftfun  7059  wfrlem17  7967  domunfican  8785  finsschain  8825  suppeqfsuppbi  8841  fsuppunbi  8848  wemapsolem  9008  wemapso  9009  wemapso2lem  9010  cantnf  9150  enfin2i  9737  ttukeylem7  9931  fpwwe2lem2  10048  fpwwe2lem9  10054  fpwwe2lem12  10057  fpwwelem  10061  distrlem4pr  10442  mulcmpblnr  10487  prsrlem1  10488  addsrmo  10489  mulsrmo  10490  divdivdiv  11335  divsubdiv  11350  lediv12a  11527  xmullem  12652  xlemul1a  12676  seqcaopr  13402  leexp2r  13533  hashf1lem1  13808  hashf1lem2  13809  fi1uzind  13850  brfi1indALT  13853  wrd2ind  14080  swrdccat  14092  cshweqrep  14178  summolem2  15068  summo  15069  prodmolem2  15284  prodmo  15285  bezoutlem3  15884  bezoutlem4  15885  qredeu  15997  pcadd  16220  vdwlem9  16320  vdwlem10  16321  ramub1lem2  16358  ramub1  16359  cofucl  17153  setcmon  17342  poslubmo  17751  posglbmo  17752  grprcan  18082  isnsg3  18257  ghmpreima  18325  gaorber  18383  psgneu  18570  odcau  18665  lsmsubm  18714  lsmmod  18737  efgsfo  18801  ablfaclem3  19145  ringpropd  19268  islmodd  19576  lmodprop2d  19632  lss1d  19671  assamulgscmlem2  20064  mplcoe1  20181  mplcoe5  20184  evlslem1  20230  lindff1  20899  islindf4  20917  mdetunilem7  21162  mdetunilem8  21163  mdetunilem9  21164  mdetuni0  21165  mdetmul  21167  ppttop  21550  epttop  21552  cnhaus  21897  isreg2  21920  cncmp  21935  1stcfb  21988  2ndcomap  22001  cldllycmp  22038  txcls  22147  ptclsg  22158  ptcnp  22165  txdis1cn  22178  txlly  22179  txnlly  22180  pthaus  22181  txhaus  22190  txkgen  22195  xkohaus  22196  xkococnlem  22202  xkococn  22203  fgabs  22422  rnelfm  22496  hausflimi  22523  hausflim  22524  alexsubALTlem2  22591  alexsubALTlem4  22593  alexsubALT  22594  tgpconncomp  22655  qustgplem  22663  metequiv2  23054  met2ndci  23066  nrmmetd  23118  nlmvscnlem1  23229  reconn  23370  xrge0tsms  23376  ipcnlem1  23782  minveclem3  23966  pmltpc  23985  ovolicc2lem5  24056  ovolicc2  24057  uniioombllem6  24123  dyadmbllem  24134  vitalilem3  24145  mbfmullem  24260  itg2split  24284  itg2mono  24288  dvlip2  24526  lhop1  24545  dvcnvrelem1  24548  ftc1lem6  24572  itgsubst  24580  dgrco  24799  plyexmo  24836  ulmdvlem3  24924  abelthlem2  24954  abelthlem8  24961  dvdsmulf1o  25704  chpchtsum  25728  dchrptlem2  25774  2sqlem5  25931  2sqlem9  25936  2sqb  25941  pntrlog2bnd  26093  pntibndlem3  26101  pntlemp  26119  pnt3  26121  tgjustf  26192  hlcgreu  26337  mirreu3  26373  cgraswap  26539  cgracom  26541  cgratr  26542  flatcgra  26543  acopyeu  26553  axsegcon  26646  ax5seglem9  26656  axeuclid  26682  axcontlem12  26694  clwwlkf1  27761  n4cyclfrgr  28003  frgrnbnb  28005  ablo4  28260  smcnlem  28407  pjhthmo  29012  pjpjpre  29129  3oalem2  29373  lnconi  29743  atom1d  30063  resf1o  30398  xrge0tsmsd  30625  ballotlemfc0  31655  ballotlemfcc  31656  pconnconn  32381  cvmfolem  32429  cvmliftmo  32434  cvmliftlem7  32441  cvmlift2lem10  32462  cvmlift3lem8  32476  noresle  33103  lineext  33440  linecgr  33445  btwnconn1lem10  33460  btwnconn1lem11  33461  btwnconn3  33467  brsegle  33472  seglecgr12im  33474  segleantisym  33479  outsideoftr  33493  outsideofeq  33494  outsideofeu  33495  linethru  33517  finminlem  33569  neibastop2lem  33611  isbasisrelowllem1  34524  isbasisrelowllem2  34525  mblfinlem3  34817  bddiblnc  34848  ftc1cnnc  34852  isbnd3  34949  heibor1lem  34974  crngm4  35168  cvlcvr1  36361  4atlem12  36634  paddasslem12  36853  paddasslem13  36854  lhpexle2lem  37031  trlord  37591  cdlemkid4  37956  dihopelvalcpre  38270  dihmeetlem1N  38312  dihglblem5apreN  38313  dihmeetlem6  38331  dih1dimatlem0  38350  dihjatcclem4  38443  mzpcl2  39211  mzpmfp  39228  mzpcompact2lem  39232  diophin  39253  pell14qrmulcl  39344  hbtlem2  39608  iunrelexpuztr  39948  stoweidlem61  42231  fourierdlem92  42368  euoreqb  43193  prproropf1olem3  43518  prproropf1olem4  43519  fpprwpprb  43756  snlindsntor  44428  elfzolborelfzop1  44476  nn0sumshdiglemB  44582
  Copyright terms: Public domain W3C validator