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

Theorem simpl12 1034
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 989 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ps )
21adantr 453 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  pythagtriplem4  13231  br8  25414  brbtwn2  25879  ax5seg  25912  ifscgr  26013  seglecgr12im  26079  lkrshp  30077  atlatle  30292  cvlcvr1  30311  atbtwn  30417  3dimlem3  30432  3dimlem3OLDN  30433  1cvratex  30444  llnmlplnN  30510  4atlem3  30567  4atlem3a  30568  4atlem11  30580  4atlem12  30583  cdlemb  30765  paddasslem4  30794  paddasslem10  30800  pmodlem1  30817  llnexchb2lem  30839  arglem1N  31161  cdlemd4  31172  cdlemd  31178  cdleme16  31256  cdleme20  31295  cdleme21k  31309  cdleme22cN  31313  cdleme27N  31340  cdleme28c  31343  cdleme29ex  31345  cdleme32fva  31408  cdleme40n  31439  cdlemg15a  31626  cdlemg15  31627  cdlemg16ALTN  31629  cdlemg16z  31630  cdlemg20  31656  cdlemg22  31658  cdlemg29  31676  cdlemg38  31686  cdlemk33N  31880  cdlemk56  31942
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator