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

Theorem simpl33 1040
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 995 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ch )
21adantr 452 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  br8  25335  ax5seglem3a  25781  ax5seg  25789  cgrextend  25854  segconeq  25856  trisegint  25874  ifscgr  25890  cgrsub  25891  btwnxfr  25902  seglecgr12im  25956  segletr  25960  atbtwn  29940  4atlem10b  30099  4atlem11  30103  4atlem12  30106  2lplnj  30114  paddasslem4  30317  paddasslem7  30320  pmodlem1  30340  4atex2  30571  trlval3  30681  arglem1N  30684  cdleme0moN  30719  cdleme20  30818  cdleme21j  30830  cdleme28c  30866  cdleme38n  30958  cdlemg6c  31114  cdlemg6  31117  cdlemg7N  31120  cdlemg16  31151  cdlemg16ALTN  31152  cdlemg16zz  31154  cdlemg20  31179  cdlemg22  31181  cdlemg37  31183  cdlemg31d  31194  cdlemg29  31199  cdlemg33b  31201  cdlemg33  31205  cdlemg46  31229  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