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

Theorem simpl12 1082
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 1037 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ps )
21adantr 467 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  pythagtriplem4  14766  pmatcollpw1lem1  19794  pmatcollpw1  19796  mp2pm2mplem2  19827  brbtwn2  24931  ax5seg  24964  br8  30401  ifscgr  30814  seglecgr12im  30880  lkrshp  32638  atlatle  32853  cvlcvr1  32872  atbtwn  32978  3dimlem3  32993  3dimlem3OLDN  32994  1cvratex  33005  llnmlplnN  33071  4atlem3  33128  4atlem3a  33129  4atlem11  33141  4atlem12  33144  cdlemb  33326  paddasslem4  33355  paddasslem10  33361  pmodlem1  33378  llnexchb2lem  33400  arglem1N  33723  cdlemd4  33734  cdlemd  33740  cdleme16  33818  cdleme20  33858  cdleme21k  33872  cdleme22cN  33876  cdleme27N  33903  cdleme28c  33906  cdleme29ex  33908  cdleme32fva  33971  cdleme40n  34002  cdlemg15a  34189  cdlemg15  34190  cdlemg16ALTN  34192  cdlemg16z  34193  cdlemg20  34219  cdlemg22  34221  cdlemg29  34239  cdlemg38  34249  cdlemk33N  34443  cdlemk56  34505  fourierdlem77  37915
  Copyright terms: Public domain W3C validator