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

Theorem simpl22 1067
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 1022 . 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 965
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 967
This theorem is referenced by:  brbtwn2  23173  ax5seg  23206  axpasch  23209  axeuclid  23231  br8d  25964  br8  27588  cgrextend  28061  segconeq  28063  trisegint  28081  ifscgr  28097  cgrsub  28098  cgrxfr  28108  lineext  28129  seglecgr12im  28163  segletr  28167  lineunray  28200  lineelsb2  28201  cvrcmp  33024  cvlatexch3  33079  cvlsupr2  33084  atcvrj2b  33172  atexchcvrN  33180  3dim1  33207  3dim2  33208  3atlem3  33225  3atlem5  33227  lplnnle2at  33281  2llnjaN  33306  4atlem3  33336  4atlem10b  33345  4atlem12  33352  2llnma3r  33528  paddasslem4  33563  paddasslem7  33566  paddasslem8  33567  paddasslem12  33571  paddasslem13  33572  paddasslem15  33574  pmodlem1  33586  pmodlem2  33587  atmod1i1m  33598  llnexchb2lem  33608  4atex2  33817  ltrnatlw  33923  trlval4  33928  arglem1N  33930  cdlemd4  33941  cdlemd5  33942  cdleme0moN  33965  cdleme16  34025  cdleme20  34064  cdleme21k  34078  cdleme27N  34109  cdleme28c  34112  cdleme43fsv1snlem  34160  cdleme38n  34204  cdleme40n  34208  cdleme41snaw  34216  cdlemg6c  34360  cdlemg8c  34369  cdlemg8  34371  cdlemg12e  34387  cdlemg16  34397  cdlemg16ALTN  34398  cdlemg16z  34399  cdlemg16zz  34400  cdlemg18a  34418  cdlemg20  34425  cdlemg22  34427  cdlemg37  34429  cdlemg31d  34440  cdlemg33  34451  cdlemg38  34455  cdlemg44b  34472  cdlemk38  34655  cdlemk35s-id  34678  cdlemk39s-id  34680  cdlemk53b  34696  cdlemk55  34701  cdlemk35u  34704  cdlemk55u  34706  cdlemn11pre  34951
  Copyright terms: Public domain W3C validator