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

Theorem simpl31 1036
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 991 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ph )
21adantr 451 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  br8  23524  ax5seglem3a  23969  ax5seg  23977  cgrextend  24042  segconeq  24044  trisegint  24062  ifscgr  24078  cgrsub  24079  btwnxfr  24090  seglecgr12im  24144  segletr  24148  isconcl5a  25513  atbtwn  29008  3dim1  29029  2llnjaN  29128  4atlem10b  29167  4atlem11  29171  4atlem12  29174  2lplnj  29182  paddasslem4  29385  pmodlem1  29408  4atex2  29639  trlval3  29749  arglem1N  29752  cdleme0moN  29787  cdleme17b  29849  cdleme20  29886  cdleme21j  29898  cdleme28c  29934  cdleme35h2  30019  cdlemg6c  30182  cdlemg6  30185  cdlemg7N  30188  cdlemg8c  30191  cdlemg11a  30199  cdlemg11b  30204  cdlemg12e  30209  cdlemg16  30219  cdlemg16ALTN  30220  cdlemg16zz  30222  cdlemg20  30247  cdlemg22  30249  cdlemg37  30251  cdlemg31d  30262  cdlemg33b  30269  cdlemg33  30273  cdlemg39  30278  cdlemg42  30291  cdlemk25-3  30466  cdlemk33N  30471  cdlemk53b  30518
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