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

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

Proof of Theorem simp11r
StepHypRef Expression
1 simp1r 1013 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant1 1009 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  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:  pceu  13925  maduf  18459  nllyrest  19102  exatleN  33060  2llnjaN  33222  2lplnja  33275  dalemceb  33294  pclfinN  33556  lhpexle3lem  33667  lhpmcvr5N  33683  lhpmcvr6N  33684  lhp2at0  33688  4atexlemw  33704  cdlemd2  33855  cdlemd4  33857  cdleme7aa  33898  cdleme7c  33901  cdleme7d  33902  cdleme7e  33903  cdleme7ga  33904  cdleme7  33905  cdleme15a  33930  cdleme15b  33931  cdleme15d  33933  cdleme15  33934  cdleme16b  33935  cdleme16c  33936  cdleme16d  33937  cdleme16e  33938  cdleme16f  33939  cdleme18d  33951  cdleme19b  33960  cdleme19d  33962  cdleme19e  33963  cdleme20d  33968  cdleme20e  33969  cdleme20f  33970  cdleme20g  33971  cdleme20h  33972  cdleme20j  33974  cdleme20k  33975  cdleme20l1  33976  cdleme20l2  33977  cdleme20l  33978  cdleme20m  33979  cdleme21c  33983  cdleme21ct  33985  cdleme22cN  33998  cdleme22f  34002  cdleme22g  34004  cdleme23a  34005  cdleme23b  34006  cdleme23c  34007  cdleme25a  34009  cdleme25c  34011  cdleme25dN  34012  cdleme26ee  34016  cdleme26eALTN  34017  cdleme27N  34025  cdleme28a  34026  cdleme28b  34027  cdleme29ex  34030  cdlemefr29exN  34058  cdleme32b  34098  cdleme32c  34099  cdleme32e  34101  cdleme35b  34106  cdleme35c  34107  cdleme35d  34108  cdleme35e  34109  cdleme35f  34110  cdleme42h  34138  cdleme42i  34139  cdleme42k  34140  cdleme48bw  34158  cdlemeg46frv  34181  cdlemeg46vrg  34183  cdlemeg46rgv  34184  cdlemeg46req  34185  cdlemf1  34217  trlord  34225  cdlemg7fvbwN  34263  cdlemg10  34297  cdlemg12e  34303  cdlemg12f  34304  cdlemg19a  34339  cdlemg31c  34355  cdlemg33c0  34358  cdlemg35  34369  tendococl  34428  cdlemh2  34472  cdlemh  34473  cdlemi  34476  cdlemk5  34492  cdlemk7  34504  cdlemk11  34505  cdlemk5u  34517  cdlemkj  34519  cdlemkuv2  34523  cdlemk7u  34526  cdlemk11u  34527  cdlemk26-3  34562  cdlemk11t  34602  cdlemk52  34610  cdlemk53a  34611  dihord1  34875  dihord2a  34876  dihord2b  34877  dihord11b  34879  dihord11c  34881  dihord2pre  34882  dihord2pre2  34883  dihord5apre  34919  dihmeetlem1N  34947  dihglblem2N  34951  dihglblem3N  34952  dihglbcpreN  34957  dihmeetlem3N  34962  dihjatc1  34968
  Copyright terms: Public domain W3C validator