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

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

Proof of Theorem simpl21
StepHypRef Expression
1 simp21 990 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ph )
21adantr 452 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  br8  25139  brbtwn2  25560  ax5seglem3a  25585  ax5seg  25593  axpasch  25596  axeuclid  25618  cgrextend  25658  segconeq  25660  trisegint  25678  ifscgr  25694  cgrsub  25695  cgrxfr  25705  lineext  25726  seglecgr12im  25760  segletr  25764  lineunray  25797  lineelsb2  25798  cvrcmp  29400  cvlatexch3  29455  cvlsupr2  29460  atexchcvrN  29556  3dim1  29583  3dim2  29584  ps-1  29593  ps-2  29594  3atlem3  29601  3atlem5  29603  lplnnle2at  29657  lplnllnneN  29672  2llnjaN  29682  4atlem3  29712  4atlem10b  29721  4atlem12  29728  2llnma3r  29904  paddasslem4  29939  paddasslem7  29942  paddasslem8  29943  paddasslem12  29947  paddasslem13  29948  pmodlem1  29962  pmodlem2  29963  llnexchb2lem  29984  4atex2  30193  ltrnatlw  30299  trlval4  30304  arglem1N  30306  cdlemd4  30317  cdlemd5  30318  cdleme0moN  30341  cdleme16  30401  cdleme20  30440  cdleme21j  30452  cdleme21k  30454  cdleme27N  30485  cdleme28c  30488  cdleme43fsv1snlem  30536  cdleme38n  30580  cdleme40n  30584  cdleme41snaw  30592  cdlemg6c  30736  cdlemg8c  30745  cdlemg8  30747  cdlemg12e  30763  cdlemg16  30773  cdlemg16ALTN  30774  cdlemg16z  30775  cdlemg16zz  30776  cdlemg18a  30794  cdlemg20  30801  cdlemg22  30803  cdlemg37  30805  cdlemg27b  30812  cdlemg31d  30816  cdlemg33  30827  cdlemg38  30831  cdlemg44b  30848  cdlemk38  31031  cdlemk35s-id  31054  cdlemk39s-id  31056  cdlemk55  31077  cdlemk35u  31080  cdlemk55u  31082  cdleml3N  31094  cdlemn11pre  31327
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