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

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

Proof of Theorem simpl33
StepHypRef Expression
1 simp33 994 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ch )
21adantr 451 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 935
This theorem is referenced by:  br8  24939  ax5seglem3a  25385  ax5seg  25393  cgrextend  25458  segconeq  25460  trisegint  25478  ifscgr  25494  cgrsub  25495  btwnxfr  25506  seglecgr12im  25560  segletr  25564  atbtwn  29694  4atlem10b  29853  4atlem11  29857  4atlem12  29860  2lplnj  29868  paddasslem4  30071  paddasslem7  30074  pmodlem1  30094  4atex2  30325  trlval3  30435  arglem1N  30438  cdleme0moN  30473  cdleme20  30572  cdleme21j  30584  cdleme28c  30620  cdleme38n  30712  cdlemg6c  30868  cdlemg6  30871  cdlemg7N  30874  cdlemg16  30905  cdlemg16ALTN  30906  cdlemg16zz  30908  cdlemg20  30933  cdlemg22  30935  cdlemg37  30937  cdlemg31d  30948  cdlemg29  30953  cdlemg33b  30955  cdlemg33  30959  cdlemg46  30983  cdlemk25-3  31152
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 937
  Copyright terms: Public domain W3C validator