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  17837  br8  23524  ax5seg  23977  cgrextend  24042  segconeq  24044  trisegint  24062  ifscgr  24078  cgrsub  24079  btwnxfr  24090  seglecgr12im  24144  segletr  24148  isconcl5a  25513  exatleN  28966  atbtwn  29008  3dim1  29029  3dim2  29030  2llnjaN  29128  4atlem10b  29167  4atlem11  29171  4atlem12  29174  2lplnj  29182  cdlemb  29356  paddasslem4  29385  pmodlem1  29408  4atex2  29639  trlval3  29749  arglem1N  29752  cdleme0moN  29787  cdleme17b  29849  cdleme20  29886  cdleme21j  29898  cdleme28c  29934  cdleme35h2  30019  cdleme38n  30026  cdlemg6c  30182  cdlemg6  30185  cdlemg7N  30188  cdlemg11a  30199  cdlemg12e  30209  cdlemg16  30219  cdlemg16ALTN  30220  cdlemg16zz  30222  cdlemg20  30247  cdlemg22  30249  cdlemg37  30251  cdlemg31d  30262  cdlemg29  30267  cdlemg33b  30269  cdlemg33  30273  cdlemg39  30278  cdlemg42  30291  cdlemk25-3  30466
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