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

Theorem simpl33 1113
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 1068 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ch )
21adantr 472 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    /\ w3a 1007
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 190  df-an 378  df-3an 1009
This theorem is referenced by:  ax5seglem3a  25039  ax5seg  25047  br8d  28294  br8  30467  cgrextend  30846  segconeq  30848  trisegint  30866  ifscgr  30882  cgrsub  30883  btwnxfr  30894  seglecgr12im  30948  segletr  30952  atbtwn  33082  4atlem10b  33241  4atlem11  33245  4atlem12  33248  2lplnj  33256  paddasslem4  33459  paddasslem7  33462  pmodlem1  33482  4atex2  33713  trlval3  33824  arglem1N  33827  cdleme0moN  33862  cdleme20  33962  cdleme21j  33974  cdleme28c  34010  cdleme38n  34102  cdlemg6c  34258  cdlemg6  34261  cdlemg7N  34264  cdlemg16  34295  cdlemg16ALTN  34296  cdlemg16zz  34298  cdlemg20  34323  cdlemg22  34325  cdlemg37  34327  cdlemg31d  34338  cdlemg29  34343  cdlemg33b  34345  cdlemg33  34349  cdlemg46  34373  cdlemk25-3  34542
  Copyright terms: Public domain W3C validator