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

Theorem simpl31 1095
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpl31  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et )  ->  ph )

Proof of Theorem simpl31
StepHypRef Expression
1 simp31 1050 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ph )
21adantr 471 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991
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 377  df-3an 993
This theorem is referenced by:  ax5seglem3a  25016  ax5seg  25024  br8d  28271  br8  30446  cgrextend  30825  segconeq  30827  trisegint  30845  ifscgr  30861  cgrsub  30862  btwnxfr  30873  seglecgr12im  30927  segletr  30931  atbtwn  33057  3dim1  33078  2llnjaN  33177  4atlem10b  33216  4atlem11  33220  4atlem12  33223  2lplnj  33231  paddasslem4  33434  pmodlem1  33457  4atex2  33688  trlval3  33799  arglem1N  33802  cdleme0moN  33837  cdleme17b  33899  cdleme20  33937  cdleme21j  33949  cdleme28c  33985  cdleme35h2  34070  cdlemg6c  34233  cdlemg6  34236  cdlemg7N  34239  cdlemg8c  34242  cdlemg11a  34250  cdlemg11b  34255  cdlemg12e  34260  cdlemg16  34270  cdlemg16ALTN  34271  cdlemg16zz  34273  cdlemg20  34298  cdlemg22  34300  cdlemg37  34302  cdlemg31d  34313  cdlemg33b  34320  cdlemg33  34324  cdlemg39  34329  cdlemg42  34342  cdlemk25-3  34517  cdlemk33N  34522  cdlemk53b  34569  uhgr1wlkspth  39883  usgr2wlkspth  39887
  Copyright terms: Public domain W3C validator