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

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

Proof of Theorem simprlr
StepHypRef Expression
1 simpr 473 . 2 ((𝜓𝜒) → 𝜒)
21ad2antrl 710 1 ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  fcof1  6776  fliftfun  6796  wfrlem17  7677  domunfican  8482  finsschain  8522  suppeqfsuppbi  8538  fsuppunbi  8545  wemapsolem  8704  wemapso  8705  wemapso2lem  8706  cantnf  8847  enfin2i  9438  ttukeylem7  9632  fpwwe2lem2  9749  fpwwe2lem9  9755  fpwwe2lem12  9758  fpwwelem  9762  distrlem4pr  10143  mulcmpblnr  10187  prsrlem1  10188  addsrmo  10189  mulsrmo  10190  divdivdiv  11021  divsubdiv  11036  lediv12a  11211  xmullem  12332  xlemul1a  12356  seqcaopr  13081  leexp2r  13161  hashf1lem1  13476  hashf1lem2  13477  fi1uzind  13516  brfi1indALT  13519  wrd2ind  13721  cshweqrep  13811  summolem2  14690  summo  14691  prodmolem2  14906  prodmo  14907  bezoutlem3  15497  bezoutlem4  15498  qredeu  15610  pcadd  15830  vdwlem9  15930  vdwlem10  15931  ramub1lem2  15968  ramub1  15969  cofucl  16772  setcmon  16961  poslubmo  17371  posglbmo  17372  grprcan  17680  isnsg3  17850  ghmpreima  17904  gaorber  17962  psgneu  18147  odcau  18240  lsmsubm  18289  lsmmod  18309  efgsfo  18373  ablfaclem3  18708  ringpropd  18804  islmodd  19093  lmodprop2d  19149  lss1d  19190  assamulgscmlem2  19578  mplcoe1  19694  mplcoe5  19697  evlslem1  19743  lindff1  20390  islindf4  20408  mdetunilem7  20656  mdetunilem8  20657  mdetunilem9  20658  mdetuni0  20659  mdetmul  20661  ppttop  21046  epttop  21048  cnhaus  21393  isreg2  21416  cncmp  21430  1stcfb  21483  2ndcomap  21496  cldllycmp  21533  txcls  21642  ptclsg  21653  ptcnp  21660  txdis1cn  21673  txlly  21674  txnlly  21675  pthaus  21676  txhaus  21685  txkgen  21690  xkohaus  21691  xkococnlem  21697  xkococn  21698  fgabs  21917  rnelfm  21991  hausflimi  22018  hausflim  22019  alexsubALTlem2  22086  alexsubALTlem4  22088  alexsubALT  22089  tgpconncomp  22150  qustgplem  22158  metequiv2  22549  met2ndci  22561  nrmmetd  22613  nlmvscnlem1  22724  reconn  22865  xrge0tsms  22871  ipcnlem1  23277  minveclem3  23435  pmltpc  23454  ovolicc2lem5  23525  ovolicc2  23526  uniioombllem6  23592  dyadmbllem  23603  vitalilem3  23614  mbfmullem  23729  itg2split  23753  itg2mono  23757  dvlip2  23995  lhop1  24014  dvcnvrelem1  24017  ftc1lem6  24041  itgsubst  24049  dgrco  24268  plyexmo  24305  ulmdvlem3  24393  abelthlem2  24423  abelthlem8  24430  dvdsmulf1o  25157  chpchtsum  25181  dchrptlem2  25227  2sqlem5  25384  2sqlem9  25389  2sqb  25394  pntrlog2bnd  25510  pntibndlem3  25518  pntlemp  25536  pnt3  25538  hlcgreu  25750  mirreu3  25786  cgraswap  25949  cgracom  25951  cgratr  25952  acopyeu  25962  axsegcon  26044  ax5seglem9  26054  axeuclid  26080  axcontlem12  26092  clwwlkf1  27221  wwlksext2clwwlkOLD  27231  frgrnbnb  27491  ablo4  27756  smcnlem  27903  pjhthmo  28512  pjpjpre  28629  3oalem2  28873  lnconi  29243  atom1d  29563  resf1o  29855  xrge0tsmsd  30133  ballotlemfc0  30902  ballotlemfcc  30903  pconnconn  31558  cvmfolem  31606  cvmliftmo  31611  cvmliftlem7  31618  cvmlift2lem10  31639  cvmlift3lem8  31653  noresle  32189  lineext  32526  linecgr  32531  btwnconn1lem10  32546  btwnconn1lem11  32547  btwnconn3  32553  brsegle  32558  seglecgr12im  32560  segleantisym  32565  outsideoftr  32579  outsideofeq  32580  outsideofeu  32581  linethru  32603  finminlem  32655  neibastop2lem  32698  isbasisrelowllem1  33538  isbasisrelowllem2  33539  mblfinlem3  33780  bddiblnc  33811  ftc1cnnc  33815  isbnd3  33913  heibor1lem  33938  crngm4  34132  cvlcvr1  35138  4atlem12  35411  paddasslem12  35630  paddasslem13  35631  lhpexle2lem  35808  trlord  36368  cdlemkid4  36733  dihopelvalcpre  37047  dihmeetlem1N  37089  dihglblem5apreN  37090  dihmeetlem6  37108  dih1dimatlem0  37127  dihjatcclem4  37220  mzpcl2  37813  mzpmfp  37830  mzpcompact2lem  37834  diophin  37856  pell14qrmulcl  37947  hbtlem2  38213  iunrelexpuztr  38529  stoweidlem61  40775  fourierdlem92  40912  snlindsntor  42846  elfzolborelfzop1  42895  nn0sumshdiglemB  43000
  Copyright terms: Public domain W3C validator