MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpl32 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  18145  br8  25335  ax5seg  25789  cgrextend  25854  segconeq  25856  trisegint  25874  ifscgr  25890  cgrsub  25891  btwnxfr  25902  seglecgr12im  25956  segletr  25960  exatleN  29898  atbtwn  29940  3dim1  29961  3dim2  29962  2llnjaN  30060  4atlem10b  30099  4atlem11  30103  4atlem12  30106  2lplnj  30114  cdlemb  30288  paddasslem4  30317  pmodlem1  30340  4atex2  30571  trlval3  30681  arglem1N  30684  cdleme0moN  30719  cdleme17b  30781  cdleme20  30818  cdleme21j  30830  cdleme28c  30866  cdleme35h2  30951  cdleme38n  30958  cdlemg6c  31114  cdlemg6  31117  cdlemg7N  31120  cdlemg11a  31131  cdlemg12e  31141  cdlemg16  31151  cdlemg16ALTN  31152  cdlemg16zz  31154  cdlemg20  31179  cdlemg22  31181  cdlemg37  31183  cdlemg31d  31194  cdlemg29  31199  cdlemg33b  31201  cdlemg33  31205  cdlemg39  31210  cdlemg42  31223  cdlemk25-3  31398
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