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

Theorem simpl12 1033
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl12  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ps )

Proof of Theorem simpl12
StepHypRef Expression
1 simp12 988 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ps )
21adantr 452 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  pythagtriplem4  13156  br8  25335  brbtwn2  25756  ax5seg  25789  ifscgr  25890  seglecgr12im  25956  lkrshp  29600  atlatle  29815  cvlcvr1  29834  atbtwn  29940  3dimlem3  29955  3dimlem3OLDN  29956  1cvratex  29967  llnmlplnN  30033  4atlem3  30090  4atlem3a  30091  4atlem11  30103  4atlem12  30106  cdlemb  30288  paddasslem4  30317  paddasslem10  30323  pmodlem1  30340  llnexchb2lem  30362  arglem1N  30684  cdlemd4  30695  cdlemd  30701  cdleme16  30779  cdleme20  30818  cdleme21k  30832  cdleme22cN  30836  cdleme27N  30863  cdleme28c  30866  cdleme29ex  30868  cdleme32fva  30931  cdleme40n  30962  cdlemg15a  31149  cdlemg15  31150  cdlemg16ALTN  31152  cdlemg16z  31153  cdlemg20  31179  cdlemg22  31181  cdlemg29  31199  cdlemg38  31209  cdlemk33N  31403  cdlemk56  31465
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator