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

Theorem simpl32 1039
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 994 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ps )
21adantr 452 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  tsmsxp  18184  br8  25379  ax5seg  25877  cgrextend  25942  segconeq  25944  trisegint  25962  ifscgr  25978  cgrsub  25979  btwnxfr  25990  seglecgr12im  26044  segletr  26048  exatleN  30201  atbtwn  30243  3dim1  30264  3dim2  30265  2llnjaN  30363  4atlem10b  30402  4atlem11  30406  4atlem12  30409  2lplnj  30417  cdlemb  30591  paddasslem4  30620  pmodlem1  30643  4atex2  30874  trlval3  30984  arglem1N  30987  cdleme0moN  31022  cdleme17b  31084  cdleme20  31121  cdleme21j  31133  cdleme28c  31169  cdleme35h2  31254  cdleme38n  31261  cdlemg6c  31417  cdlemg6  31420  cdlemg7N  31423  cdlemg11a  31434  cdlemg12e  31444  cdlemg16  31454  cdlemg16ALTN  31455  cdlemg16zz  31457  cdlemg20  31482  cdlemg22  31484  cdlemg37  31486  cdlemg31d  31497  cdlemg29  31502  cdlemg33b  31504  cdlemg33  31508  cdlemg39  31513  cdlemg42  31526  cdlemk25-3  31701
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