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

Theorem simp11r 1108
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 1021 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant1 1017 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  pceu  14228  maduf  18926  nllyrest  19769  limsupre  31199  exatleN  34209  2llnjaN  34371  2lplnja  34424  dalemceb  34443  pclfinN  34705  lhpexle3lem  34816  lhpmcvr5N  34832  lhpmcvr6N  34833  lhp2at0  34837  4atexlemw  34853  cdlemd2  35004  cdlemd4  35006  cdleme7aa  35047  cdleme7c  35050  cdleme7d  35051  cdleme7e  35052  cdleme7ga  35053  cdleme7  35054  cdleme15a  35079  cdleme15b  35080  cdleme15d  35082  cdleme15  35083  cdleme16b  35084  cdleme16c  35085  cdleme16d  35086  cdleme16e  35087  cdleme16f  35088  cdleme18d  35100  cdleme19b  35109  cdleme19d  35111  cdleme19e  35112  cdleme20d  35117  cdleme20e  35118  cdleme20f  35119  cdleme20g  35120  cdleme20h  35121  cdleme20j  35123  cdleme20k  35124  cdleme20l1  35125  cdleme20l2  35126  cdleme20l  35127  cdleme20m  35128  cdleme21c  35132  cdleme21ct  35134  cdleme22cN  35147  cdleme22f  35151  cdleme22g  35153  cdleme23a  35154  cdleme23b  35155  cdleme23c  35156  cdleme25a  35158  cdleme25c  35160  cdleme25dN  35161  cdleme26ee  35165  cdleme26eALTN  35166  cdleme27N  35174  cdleme28a  35175  cdleme28b  35176  cdleme29ex  35179  cdlemefr29exN  35207  cdleme32b  35247  cdleme32c  35248  cdleme32e  35250  cdleme35b  35255  cdleme35c  35256  cdleme35d  35257  cdleme35e  35258  cdleme35f  35259  cdleme42h  35287  cdleme42i  35288  cdleme42k  35289  cdleme48bw  35307  cdlemeg46frv  35330  cdlemeg46vrg  35332  cdlemeg46rgv  35333  cdlemeg46req  35334  cdlemf1  35366  trlord  35374  cdlemg7fvbwN  35412  cdlemg10  35446  cdlemg12e  35452  cdlemg12f  35453  cdlemg19a  35488  cdlemg31c  35504  cdlemg33c0  35507  cdlemg35  35518  tendococl  35577  cdlemh2  35621  cdlemh  35622  cdlemi  35625  cdlemk5  35641  cdlemk7  35653  cdlemk11  35654  cdlemk5u  35666  cdlemkj  35668  cdlemkuv2  35672  cdlemk7u  35675  cdlemk11u  35676  cdlemk26-3  35711  cdlemk11t  35751  cdlemk52  35759  cdlemk53a  35760  dihord1  36024  dihord2a  36025  dihord2b  36026  dihord11b  36028  dihord11c  36030  dihord2pre  36031  dihord2pre2  36032  dihord5apre  36068  dihmeetlem1N  36096  dihglblem2N  36100  dihglblem3N  36101  dihglbcpreN  36106  dihmeetlem3N  36111  dihjatc1  36117
  Copyright terms: Public domain W3C validator