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

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

Proof of Theorem simpl32
StepHypRef Expression
1 simp32 992 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ps )
21adantr 451 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  tsmsxp  17853  br8  24184  ax5seg  24638  cgrextend  24703  segconeq  24705  trisegint  24723  ifscgr  24739  cgrsub  24740  btwnxfr  24751  seglecgr12im  24805  segletr  24809  isconcl5a  26204  exatleN  30215  atbtwn  30257  3dim1  30278  3dim2  30279  2llnjaN  30377  4atlem10b  30416  4atlem11  30420  4atlem12  30423  2lplnj  30431  cdlemb  30605  paddasslem4  30634  pmodlem1  30657  4atex2  30888  trlval3  30998  arglem1N  31001  cdleme0moN  31036  cdleme17b  31098  cdleme20  31135  cdleme21j  31147  cdleme28c  31183  cdleme35h2  31268  cdleme38n  31275  cdlemg6c  31431  cdlemg6  31434  cdlemg7N  31437  cdlemg11a  31448  cdlemg12e  31458  cdlemg16  31468  cdlemg16ALTN  31469  cdlemg16zz  31471  cdlemg20  31496  cdlemg22  31498  cdlemg37  31500  cdlemg31d  31511  cdlemg29  31516  cdlemg33b  31518  cdlemg33  31522  cdlemg39  31527  cdlemg42  31540  cdlemk25-3  31715
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