MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpl33 Structured version   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  25379  ax5seglem3a  25869  ax5seg  25877  cgrextend  25942  segconeq  25944  trisegint  25962  ifscgr  25978  cgrsub  25979  btwnxfr  25990  seglecgr12im  26044  segletr  26048  atbtwn  30243  4atlem10b  30402  4atlem11  30406  4atlem12  30409  2lplnj  30417  paddasslem4  30620  paddasslem7  30623  pmodlem1  30643  4atex2  30874  trlval3  30984  arglem1N  30987  cdleme0moN  31022  cdleme20  31121  cdleme21j  31133  cdleme28c  31169  cdleme38n  31261  cdlemg6c  31417  cdlemg6  31420  cdlemg7N  31423  cdlemg16  31454  cdlemg16ALTN  31455  cdlemg16zz  31457  cdlemg20  31482  cdlemg22  31484  cdlemg37  31486  cdlemg31d  31497  cdlemg29  31502  cdlemg33b  31504  cdlemg33  31508  cdlemg46  31532  cdlemk25-3  31701
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