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  12996  nllyrest  17318  exatleN  29662  2llnjaN  29824  2lplnja  29877  dalemceb  29896  pclfinN  30158  lhpexle3lem  30269  lhpmcvr5N  30285  lhpmcvr6N  30286  lhp2at0  30290  4atexlemw  30306  cdlemd2  30457  cdlemd4  30459  cdleme7aa  30500  cdleme7c  30503  cdleme7d  30504  cdleme7e  30505  cdleme7ga  30506  cdleme7  30507  cdleme15a  30532  cdleme15b  30533  cdleme15d  30535  cdleme15  30536  cdleme16b  30537  cdleme16c  30538  cdleme16d  30539  cdleme16e  30540  cdleme16f  30541  cdleme18d  30553  cdleme19b  30562  cdleme19d  30564  cdleme19e  30565  cdleme20d  30570  cdleme20e  30571  cdleme20f  30572  cdleme20g  30573  cdleme20h  30574  cdleme20j  30576  cdleme20k  30577  cdleme20l1  30578  cdleme20l2  30579  cdleme20l  30580  cdleme20m  30581  cdleme21c  30585  cdleme21ct  30587  cdleme22cN  30600  cdleme22f  30604  cdleme22g  30606  cdleme23a  30607  cdleme23b  30608  cdleme23c  30609  cdleme25a  30611  cdleme25c  30613  cdleme25dN  30614  cdleme26ee  30618  cdleme26eALTN  30619  cdleme27N  30627  cdleme28a  30628  cdleme28b  30629  cdleme29ex  30632  cdlemefr29exN  30660  cdleme32b  30700  cdleme32c  30701  cdleme32e  30703  cdleme35b  30708  cdleme35c  30709  cdleme35d  30710  cdleme35e  30711  cdleme35f  30712  cdleme42h  30740  cdleme42i  30741  cdleme42k  30742  cdleme48bw  30760  cdlemeg46frv  30783  cdlemeg46vrg  30785  cdlemeg46rgv  30786  cdlemeg46req  30787  cdlemf1  30819  trlord  30827  cdlemg7fvbwN  30865  cdlemg10  30899  cdlemg12e  30905  cdlemg12f  30906  cdlemg19a  30941  cdlemg31c  30957  cdlemg33c0  30960  cdlemg35  30971  tendococl  31030  cdlemh2  31074  cdlemh  31075  cdlemi  31078  cdlemk5  31094  cdlemk7  31106  cdlemk11  31107  cdlemk5u  31119  cdlemkj  31121  cdlemkuv2  31125  cdlemk7u  31128  cdlemk11u  31129  cdlemk26-3  31164  cdlemk11t  31204  cdlemk52  31212  cdlemk53a  31213  dihord1  31477  dihord2a  31478  dihord2b  31479  dihord11b  31481  dihord11c  31483  dihord2pre  31484  dihord2pre2  31485  dihord5apre  31521  dihmeetlem1N  31549  dihglblem2N  31553  dihglblem3N  31554  dihglbcpreN  31559  dihmeetlem3N  31564  dihjatc1  31570
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