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

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

Proof of Theorem simpl3l
StepHypRef Expression
1 simp3l 1024 . 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  xaddass  11470  xlemul2a  11510  dvdsadd2b  14028  pockthg  14424  psgnunilem4  16522  efgred  16766  ptbasin  20078  basqtop  20212  xrsmopn  21317  axpasch  24244  axcontlem4  24270  br4  29187  btwnintr  29669  btwnexch3  29670  btwnouttr2  29672  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  limcleqr  31650  fourierdlem42  31931  cvrcmp  35008  atcvrj2b  35156  3dimlem3  35185  3dimlem3OLDN  35186  3dim3  35193  ps-1  35201  lplnnle2at  35265  2llnm3N  35293  lvolnle3at  35306  4atlem0a  35317  4atlem3  35320  4atlem3a  35321  lnatexN  35503  paddasslem8  35551  paddasslem9  35552  paddasslem10  35553  paddasslem12  35555  paddasslem13  35556  lhp2lt  35725  lhpexle2lem  35733  lhpexle3  35736  lhpmcvr3  35749  lhpat3  35770  4atex  35800  trlval2  35888  ltrnideq  35900  ltrnatlw  35908  trlnle  35911  trlval4  35913  cdlemd4  35926  cdlemd5  35927  cdleme16  36010  cdleme21  36063  cdleme21k  36064  cdleme27cl  36092  cdleme27N  36095  cdleme29ex  36100  cdleme43fsv1snlem  36146  cdleme40m  36193  cdleme46f2g2  36219  cdleme46f2g1  36220  trlord  36295  cdlemg8  36357  cdlemg15a  36381  cdlemg16z  36385  cdlemg18a  36404  cdlemg24  36414  cdlemg38  36441  cdlemg40  36443  trlcone  36454  cdlemj2  36548  tendoid0  36551  tendoconid  36555  cdlemk34  36636  cdlemk38  36641  cdlemkid4  36660  cdlemk35s-id  36664  cdlemk39s-id  36666  cdlemk53  36683  tendospcanN  36750  cdlemm10N  36845  dihvalcqpre  36962  dihopelvalcpre  36975  dihord5b  36986  dihglblem5apreN  37018  dihmeetlem16N  37049  dihmeetlem17N  37050  dvh3dim3N  37176
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