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  18099  br8  25131  ax5seg  25585  cgrextend  25650  segconeq  25652  trisegint  25670  ifscgr  25686  cgrsub  25687  btwnxfr  25698  seglecgr12im  25752  segletr  25756  exatleN  29570  atbtwn  29612  3dim1  29633  3dim2  29634  2llnjaN  29732  4atlem10b  29771  4atlem11  29775  4atlem12  29778  2lplnj  29786  cdlemb  29960  paddasslem4  29989  pmodlem1  30012  4atex2  30243  trlval3  30353  arglem1N  30356  cdleme0moN  30391  cdleme17b  30453  cdleme20  30490  cdleme21j  30502  cdleme28c  30538  cdleme35h2  30623  cdleme38n  30630  cdlemg6c  30786  cdlemg6  30789  cdlemg7N  30792  cdlemg11a  30803  cdlemg12e  30813  cdlemg16  30823  cdlemg16ALTN  30824  cdlemg16zz  30826  cdlemg20  30851  cdlemg22  30853  cdlemg37  30855  cdlemg31d  30866  cdlemg29  30871  cdlemg33b  30873  cdlemg33  30877  cdlemg39  30882  cdlemg42  30895  cdlemk25-3  31070
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