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

Theorem simpl31 1038
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 993 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ph )
21adantr 452 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  br8  25130  ax5seglem3a  25576  ax5seg  25584  cgrextend  25649  segconeq  25651  trisegint  25669  ifscgr  25685  cgrsub  25686  btwnxfr  25697  seglecgr12im  25751  segletr  25755  atbtwn  29611  3dim1  29632  2llnjaN  29731  4atlem10b  29770  4atlem11  29774  4atlem12  29777  2lplnj  29785  paddasslem4  29988  pmodlem1  30011  4atex2  30242  trlval3  30352  arglem1N  30355  cdleme0moN  30390  cdleme17b  30452  cdleme20  30489  cdleme21j  30501  cdleme28c  30537  cdleme35h2  30622  cdlemg6c  30785  cdlemg6  30788  cdlemg7N  30791  cdlemg8c  30794  cdlemg11a  30802  cdlemg11b  30807  cdlemg12e  30812  cdlemg16  30822  cdlemg16ALTN  30823  cdlemg16zz  30825  cdlemg20  30850  cdlemg22  30852  cdlemg37  30854  cdlemg31d  30865  cdlemg33b  30872  cdlemg33  30876  cdlemg39  30881  cdlemg42  30894  cdlemk25-3  31069  cdlemk33N  31074  cdlemk53b  31121
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