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

Theorem simpl33 1038
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 993 . 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 934
This theorem is referenced by:  br8  24113  ax5seglem3a  24558  ax5seg  24566  cgrextend  24631  segconeq  24633  trisegint  24651  ifscgr  24667  cgrsub  24668  btwnxfr  24679  seglecgr12im  24733  segletr  24737  isconcl5a  26101  lppotos  26144  atbtwn  29635  4atlem10b  29794  4atlem11  29798  4atlem12  29801  2lplnj  29809  paddasslem4  30012  paddasslem7  30015  pmodlem1  30035  4atex2  30266  trlval3  30376  arglem1N  30379  cdleme0moN  30414  cdleme20  30513  cdleme21j  30525  cdleme28c  30561  cdleme38n  30653  cdlemg6c  30809  cdlemg6  30812  cdlemg7N  30815  cdlemg16  30846  cdlemg16ALTN  30847  cdlemg16zz  30849  cdlemg20  30874  cdlemg22  30876  cdlemg37  30878  cdlemg31d  30889  cdlemg29  30894  cdlemg33b  30896  cdlemg33  30900  cdlemg46  30924  cdlemk25-3  31093
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 936
  Copyright terms: Public domain W3C validator