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

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

Proof of Theorem simpl22
StepHypRef Expression
1 simp22 1025 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ps )
21adantr 465 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 968
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 185  df-an 371  df-3an 970
This theorem is referenced by:  brbtwn2  23879  ax5seg  23912  axpasch  23915  axeuclid  23937  br8d  27124  br8  28750  cgrextend  29223  segconeq  29225  trisegint  29243  ifscgr  29259  cgrsub  29260  cgrxfr  29270  lineext  29291  seglecgr12im  29325  segletr  29329  lineunray  29362  lineelsb2  29363  cvrcmp  33957  cvlatexch3  34012  cvlsupr2  34017  atcvrj2b  34105  atexchcvrN  34113  3dim1  34140  3dim2  34141  3atlem3  34158  3atlem5  34160  lplnnle2at  34214  2llnjaN  34239  4atlem3  34269  4atlem10b  34278  4atlem12  34285  2llnma3r  34461  paddasslem4  34496  paddasslem7  34499  paddasslem8  34500  paddasslem12  34504  paddasslem13  34505  paddasslem15  34507  pmodlem1  34519  pmodlem2  34520  atmod1i1m  34531  llnexchb2lem  34541  4atex2  34750  ltrnatlw  34856  trlval4  34861  arglem1N  34863  cdlemd4  34874  cdlemd5  34875  cdleme0moN  34898  cdleme16  34958  cdleme20  34997  cdleme21k  35011  cdleme27N  35042  cdleme28c  35045  cdleme43fsv1snlem  35093  cdleme38n  35137  cdleme40n  35141  cdleme41snaw  35149  cdlemg6c  35293  cdlemg8c  35302  cdlemg8  35304  cdlemg12e  35320  cdlemg16  35330  cdlemg16ALTN  35331  cdlemg16z  35332  cdlemg16zz  35333  cdlemg18a  35351  cdlemg20  35358  cdlemg22  35360  cdlemg37  35362  cdlemg31d  35373  cdlemg33  35384  cdlemg38  35388  cdlemg44b  35405  cdlemk38  35588  cdlemk35s-id  35611  cdlemk39s-id  35613  cdlemk53b  35629  cdlemk55  35634  cdlemk35u  35637  cdlemk55u  35639  cdlemn11pre  35884
  Copyright terms: Public domain W3C validator