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

Theorem simpl22 1036
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 991 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ps )
21adantr 452 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  br8  25379  brbtwn2  25844  ax5seg  25877  axpasch  25880  axeuclid  25902  cgrextend  25942  segconeq  25944  trisegint  25962  ifscgr  25978  cgrsub  25979  cgrxfr  25989  lineext  26010  seglecgr12im  26044  segletr  26048  lineunray  26081  lineelsb2  26082  cvrcmp  30081  cvlatexch3  30136  cvlsupr2  30141  atcvrj2b  30229  atexchcvrN  30237  3dim1  30264  3dim2  30265  3atlem3  30282  3atlem5  30284  lplnnle2at  30338  2llnjaN  30363  4atlem3  30393  4atlem10b  30402  4atlem12  30409  2llnma3r  30585  paddasslem4  30620  paddasslem7  30623  paddasslem8  30624  paddasslem12  30628  paddasslem13  30629  paddasslem15  30631  pmodlem1  30643  pmodlem2  30644  atmod1i1m  30655  llnexchb2lem  30665  4atex2  30874  ltrnatlw  30980  trlval4  30985  arglem1N  30987  cdlemd4  30998  cdlemd5  30999  cdleme0moN  31022  cdleme16  31082  cdleme20  31121  cdleme21k  31135  cdleme27N  31166  cdleme28c  31169  cdleme43fsv1snlem  31217  cdleme38n  31261  cdleme40n  31265  cdleme41snaw  31273  cdlemg6c  31417  cdlemg8c  31426  cdlemg8  31428  cdlemg12e  31444  cdlemg16  31454  cdlemg16ALTN  31455  cdlemg16z  31456  cdlemg16zz  31457  cdlemg18a  31475  cdlemg20  31482  cdlemg22  31484  cdlemg37  31486  cdlemg31d  31497  cdlemg33  31508  cdlemg38  31512  cdlemg44b  31529  cdlemk38  31712  cdlemk35s-id  31735  cdlemk39s-id  31737  cdlemk53b  31753  cdlemk55  31758  cdlemk35u  31761  cdlemk55u  31763  cdlemn11pre  32008
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