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

Theorem simpl22 1076
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 1031 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ps )
21adantr 463 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  brbtwn2  24612  ax5seg  24645  axpasch  24648  axeuclid  24670  br8d  27886  br8  29956  cgrextend  30333  segconeq  30335  trisegint  30353  ifscgr  30369  cgrsub  30370  cgrxfr  30380  lineext  30401  seglecgr12im  30435  segletr  30439  lineunray  30472  lineelsb2  30473  cvrcmp  32281  cvlatexch3  32336  cvlsupr2  32341  atcvrj2b  32429  atexchcvrN  32437  3dim1  32464  3dim2  32465  3atlem3  32482  3atlem5  32484  lplnnle2at  32538  2llnjaN  32563  4atlem3  32593  4atlem10b  32602  4atlem12  32609  2llnma3r  32785  paddasslem4  32820  paddasslem7  32823  paddasslem8  32824  paddasslem12  32828  paddasslem13  32829  paddasslem15  32831  pmodlem1  32843  pmodlem2  32844  atmod1i1m  32855  llnexchb2lem  32865  4atex2  33074  ltrnatlw  33181  trlval4  33186  arglem1N  33188  cdlemd4  33199  cdlemd5  33200  cdleme0moN  33223  cdleme16  33283  cdleme20  33323  cdleme21k  33337  cdleme27N  33368  cdleme28c  33371  cdleme43fsv1snlem  33419  cdleme38n  33463  cdleme40n  33467  cdleme41snaw  33475  cdlemg6c  33619  cdlemg8c  33628  cdlemg8  33630  cdlemg12e  33646  cdlemg16  33656  cdlemg16ALTN  33657  cdlemg16z  33658  cdlemg16zz  33659  cdlemg18a  33677  cdlemg20  33684  cdlemg22  33686  cdlemg37  33688  cdlemg31d  33699  cdlemg33  33710  cdlemg38  33714  cdlemg44b  33731  cdlemk38  33914  cdlemk35s-id  33937  cdlemk39s-id  33939  cdlemk53b  33955  cdlemk55  33960  cdlemk35u  33963  cdlemk55u  33965  cdlemn11pre  34210
  Copyright terms: Public domain W3C validator