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

Theorem simpl12 1031
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 986 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ps )
21adantr 451 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  pythagtriplem4  12872  br8  24113  brbtwn2  24533  ax5seg  24566  ifscgr  24667  seglecgr12im  24733  islimrs4  25582  lkrshp  29295  atlatle  29510  cvlcvr1  29529  atbtwn  29635  3dimlem3  29650  3dimlem3OLDN  29651  1cvratex  29662  llnmlplnN  29728  4atlem3  29785  4atlem3a  29786  4atlem11  29798  4atlem12  29801  cdlemb  29983  paddasslem4  30012  paddasslem10  30018  pmodlem1  30035  llnexchb2lem  30057  arglem1N  30379  cdlemd4  30390  cdlemd  30396  cdleme16  30474  cdleme20  30513  cdleme21k  30527  cdleme22cN  30531  cdleme27N  30558  cdleme28c  30561  cdleme29ex  30563  cdleme32fva  30626  cdleme40n  30657  cdlemg15a  30844  cdlemg15  30845  cdlemg16ALTN  30847  cdlemg16z  30848  cdlemg20  30874  cdlemg22  30876  cdlemg29  30894  cdlemg38  30904  cdlemk33N  31098  cdlemk56  31160
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator