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

Theorem simp11r 1067
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 980 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant1 976 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  pceu  12899  nllyrest  17212  exatleN  29593  2llnjaN  29755  2lplnja  29808  dalemceb  29827  pclfinN  30089  lhpexle3lem  30200  lhpmcvr5N  30216  lhpmcvr6N  30217  lhp2at0  30221  4atexlemw  30237  cdlemd2  30388  cdlemd4  30390  cdleme7aa  30431  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme7ga  30437  cdleme7  30438  cdleme15a  30463  cdleme15b  30464  cdleme15d  30466  cdleme15  30467  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme16e  30471  cdleme16f  30472  cdleme18d  30484  cdleme19b  30493  cdleme19d  30495  cdleme19e  30496  cdleme20d  30501  cdleme20e  30502  cdleme20f  30503  cdleme20g  30504  cdleme20h  30505  cdleme20j  30507  cdleme20k  30508  cdleme20l1  30509  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme21c  30516  cdleme21ct  30518  cdleme22cN  30531  cdleme22f  30535  cdleme22g  30537  cdleme23a  30538  cdleme23b  30539  cdleme23c  30540  cdleme25a  30542  cdleme25c  30544  cdleme25dN  30545  cdleme26ee  30549  cdleme26eALTN  30550  cdleme27N  30558  cdleme28a  30559  cdleme28b  30560  cdleme29ex  30563  cdlemefr29exN  30591  cdleme32b  30631  cdleme32c  30632  cdleme32e  30634  cdleme35b  30639  cdleme35c  30640  cdleme35d  30641  cdleme35e  30642  cdleme35f  30643  cdleme42h  30671  cdleme42i  30672  cdleme42k  30673  cdleme48bw  30691  cdlemeg46frv  30714  cdlemeg46vrg  30716  cdlemeg46rgv  30717  cdlemeg46req  30718  cdlemf1  30750  trlord  30758  cdlemg7fvbwN  30796  cdlemg10  30830  cdlemg12e  30836  cdlemg12f  30837  cdlemg19a  30872  cdlemg31c  30888  cdlemg33c0  30891  cdlemg35  30902  tendococl  30961  cdlemh2  31005  cdlemh  31006  cdlemi  31009  cdlemk5  31025  cdlemk7  31037  cdlemk11  31038  cdlemk5u  31050  cdlemkj  31052  cdlemkuv2  31056  cdlemk7u  31059  cdlemk11u  31060  cdlemk26-3  31095  cdlemk11t  31135  cdlemk52  31143  cdlemk53a  31144  dihord1  31408  dihord2a  31409  dihord2b  31410  dihord11b  31412  dihord11c  31414  dihord2pre  31415  dihord2pre2  31416  dihord5apre  31452  dihmeetlem1N  31480  dihglblem2N  31484  dihglblem3N  31485  dihglbcpreN  31490  dihmeetlem3N  31495  dihjatc1  31501
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator