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

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

Proof of Theorem simpl11
StepHypRef Expression
1 simp11 1026 . 2
21adantr 465 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  pythagtriplem4  14343  tsmsxp  20657  brbtwn2  24208  ax5seg  24241  br8  29185  btwndiff  29677  ifscgr  29694  seglecgr12im  29760  fourierdlem77  31966  lkrshp  34830  cvlcvr1  35064  atbtwn  35170  3dimlem3  35185  3dimlem3OLDN  35186  1cvratex  35197  llnmlplnN  35263  4atlem3  35320  4atlem3a  35321  4atlem11  35333  4atlem12  35336  lnatexN  35503  cdlemb  35518  paddasslem4  35547  paddasslem10  35553  pmodlem1  35570  llnexchb2lem  35592  llnexchb2  35593  arglem1N  35915  cdlemd4  35926  cdlemd9  35931  cdlemd  35932  cdleme16  36010  cdleme20  36050  cdleme21i  36061  cdleme21k  36064  cdleme27N  36095  cdleme28c  36098  cdlemefrs29bpre0  36122  cdlemefrs29clN  36125  cdlemefrs32fva  36126  cdleme41sn3a  36159  cdleme32fva  36163  cdleme40n  36194  cdlemg12e  36373  cdlemg15a  36381  cdlemg15  36382  cdlemg16ALTN  36384  cdlemg16z  36385  cdlemg20  36411  cdlemg22  36413  cdlemg29  36431  cdlemg38  36441  cdlemk33N  36635  cdlemk56  36697  dihord11b  36949  dihord2pre  36952  dihord4  36985
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