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

Theorem simpl33 1090
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 1045 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ch )
21adantr 467 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 189  df-an 373  df-3an 986
This theorem is referenced by:  ax5seglem3a  24953  ax5seg  24961  br8d  28211  br8  30389  cgrextend  30768  segconeq  30770  trisegint  30788  ifscgr  30804  cgrsub  30805  btwnxfr  30816  seglecgr12im  30870  segletr  30874  atbtwn  33005  4atlem10b  33164  4atlem11  33168  4atlem12  33171  2lplnj  33179  paddasslem4  33382  paddasslem7  33385  pmodlem1  33405  4atex2  33636  trlval3  33747  arglem1N  33750  cdleme0moN  33785  cdleme20  33885  cdleme21j  33897  cdleme28c  33933  cdleme38n  34025  cdlemg6c  34181  cdlemg6  34184  cdlemg7N  34187  cdlemg16  34218  cdlemg16ALTN  34219  cdlemg16zz  34221  cdlemg20  34246  cdlemg22  34248  cdlemg37  34250  cdlemg31d  34261  cdlemg29  34266  cdlemg33b  34268  cdlemg33  34272  cdlemg46  34296  cdlemk25-3  34465
  Copyright terms: Public domain W3C validator