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  7034  fliftfun  7054  wfrlem17  7962  domunfican  8780  finsschain  8820  suppeqfsuppbi  8836  fsuppunbi  8843  wemapsolem  9003  wemapso  9004  wemapso2lem  9005  cantnf  9145  enfin2i  9732  ttukeylem7  9926  fpwwe2lem2  10043  fpwwe2lem9  10049  fpwwe2lem12  10052  fpwwelem  10056  distrlem4pr  10437  mulcmpblnr  10482  prsrlem1  10483  addsrmo  10484  mulsrmo  10485  divdivdiv  11330  divsubdiv  11345  lediv12a  11522  xmullem  12647  xlemul1a  12671  seqcaopr  13397  leexp2r  13528  hashf1lem1  13803  hashf1lem2  13804  fi1uzind  13845  brfi1indALT  13848  wrd2ind  14075  swrdccat  14087  cshweqrep  14173  summolem2  15063  summo  15064  prodmolem2  15279  prodmo  15280  bezoutlem3  15879  bezoutlem4  15880  qredeu  15992  pcadd  16215  vdwlem9  16315  vdwlem10  16316  ramub1lem2  16353  ramub1  16354  cofucl  17148  setcmon  17337  poslubmo  17746  posglbmo  17747  grprcan  18077  isnsg3  18252  ghmpreima  18320  gaorber  18378  psgneu  18565  odcau  18660  lsmsubm  18709  lsmmod  18732  efgsfo  18796  ablfaclem3  19140  ringpropd  19263  islmodd  19571  lmodprop2d  19627  lss1d  19666  assamulgscmlem2  20059  mplcoe1  20176  mplcoe5  20179  evlslem1  20225  lindff1  20894  islindf4  20912  mdetunilem7  21157  mdetunilem8  21158  mdetunilem9  21159  mdetuni0  21160  mdetmul  21162  ppttop  21545  epttop  21547  cnhaus  21892  isreg2  21915  cncmp  21930  1stcfb  21983  2ndcomap  21996  cldllycmp  22033  txcls  22142  ptclsg  22153  ptcnp  22160  txdis1cn  22173  txlly  22174  txnlly  22175  pthaus  22176  txhaus  22185  txkgen  22190  xkohaus  22191  xkococnlem  22197  xkococn  22198  fgabs  22417  rnelfm  22491  hausflimi  22518  hausflim  22519  alexsubALTlem2  22586  alexsubALTlem4  22588  alexsubALT  22589  tgpconncomp  22650  qustgplem  22658  metequiv2  23049  met2ndci  23061  nrmmetd  23113  nlmvscnlem1  23224  reconn  23365  xrge0tsms  23371  ipcnlem1  23777  minveclem3  23961  pmltpc  23980  ovolicc2lem5  24051  ovolicc2  24052  uniioombllem6  24118  dyadmbllem  24129  vitalilem3  24140  mbfmullem  24255  itg2split  24279  itg2mono  24283  dvlip2  24521  lhop1  24540  dvcnvrelem1  24543  ftc1lem6  24567  itgsubst  24575  dgrco  24794  plyexmo  24831  ulmdvlem3  24919  abelthlem2  24949  abelthlem8  24956  dvdsmulf1o  25699  chpchtsum  25723  dchrptlem2  25769  2sqlem5  25926  2sqlem9  25931  2sqb  25936  pntrlog2bnd  26088  pntibndlem3  26096  pntlemp  26114  pnt3  26116  tgjustf  26187  hlcgreu  26332  mirreu3  26368  cgraswap  26534  cgracom  26536  cgratr  26537  flatcgra  26538  acopyeu  26548  axsegcon  26641  ax5seglem9  26651  axeuclid  26677  axcontlem12  26689  clwwlkf1  27756  n4cyclfrgr  27998  frgrnbnb  28000  ablo4  28255  smcnlem  28402  pjhthmo  29007  pjpjpre  29124  3oalem2  29368  lnconi  29738  atom1d  30058  resf1o  30393  xrge0tsmsd  30620  ballotlemfc0  31650  ballotlemfcc  31651  pconnconn  32376  cvmfolem  32424  cvmliftmo  32429  cvmliftlem7  32436  cvmlift2lem10  32457  cvmlift3lem8  32471  noresle  33098  lineext  33435  linecgr  33440  btwnconn1lem10  33455  btwnconn1lem11  33456  btwnconn3  33462  brsegle  33467  seglecgr12im  33469  segleantisym  33474  outsideoftr  33488  outsideofeq  33489  outsideofeu  33490  linethru  33512  finminlem  33564  neibastop2lem  33606  isbasisrelowllem1  34519  isbasisrelowllem2  34520  mblfinlem3  34813  bddiblnc  34844  ftc1cnnc  34848  isbnd3  34945  heibor1lem  34970  crngm4  35164  cvlcvr1  36357  4atlem12  36630  paddasslem12  36849  paddasslem13  36850  lhpexle2lem  37027  trlord  37587  cdlemkid4  37952  dihopelvalcpre  38266  dihmeetlem1N  38308  dihglblem5apreN  38309  dihmeetlem6  38327  dih1dimatlem0  38346  dihjatcclem4  38439  mzpcl2  39207  mzpmfp  39224  mzpcompact2lem  39228  diophin  39249  pell14qrmulcl  39340  hbtlem2  39604  iunrelexpuztr  39944  stoweidlem61  42227  fourierdlem92  42364  euoreqb  43189  prproropf1olem3  43514  prproropf1olem4  43515  fpprwpprb  43752  snlindsntor  44424  elfzolborelfzop1  44472  nn0sumshdiglemB  44578
  Copyright terms: Public domain W3C validator