MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpl3r Unicode version

Theorem simpl3r 1052
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl3r

Proof of Theorem simpl3r
StepHypRef Expression
1 simp3r 1025 . 2
21adantr 465 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  tfisi  6693  omopth2  7252  ltmul1a  10416  xmulasslem3  11507  xadddi2  11518  dvdsadd2b  14028  pockthg  14424  psgnunilem4  16522  efgred  16766  marrepeval  19065  submaeval  19084  mdetmul  19125  minmar1eval  19151  ptbasin  20078  basqtop  20212  xrsmopn  21317  axpasch  24244  axeuclid  24266  extwwlkfablem2  25078  br4  29187  btwnouttr2  29672  trisegint  29678  cgrxfr  29705  lineext  29726  btwnconn1lem13  29749  btwnconn1lem14  29750  btwnconn3  29753  brsegle  29758  brsegle2  29759  segleantisym  29765  outsideofeu  29781  lineunray  29797  lineelsb2  29798  qirropth  30844  mzpcong  30910  jm2.26  30944  aomclem6  31005  islptre  31625  limccog  31626  limcleqr  31650  fourierdlem42  31931  elaa2  32017  cvrcmp  35008  atcvrj2b  35156  3dimlem3  35185  3dimlem3OLDN  35186  3dim3  35193  ps-1  35201  ps-2  35202  lplnnle2at  35265  2llnm3N  35293  4atlem0a  35317  4atlem3  35320  4atlem3a  35321  lnatexN  35503  paddasslem8  35551  paddasslem9  35552  paddasslem10  35553  paddasslem12  35555  paddasslem13  35556  lhpexle2lem  35733  lhpexle3  35736  lhpat3  35770  4atex  35800  trlval2  35888  trlval4  35913  cdleme16  36010  cdleme21  36063  cdleme21k  36064  cdleme27cl  36092  cdleme27N  36095  cdleme43fsv1snlem  36146  cdleme48fvg  36226  cdlemg8  36357  cdlemg15a  36381  cdlemg16z  36385  cdlemg24  36414  cdlemg38  36441  cdlemg40  36443  trlcone  36454  cdlemj2  36548  tendoid0  36551  tendoconid  36555  cdlemk34  36636  cdlemk38  36641  cdlemkid4  36660  cdlemk53  36683  tendospcanN  36750  dihvalcqpre  36962  dihmeetlem15N  37048
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator