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

Theorem simp11r 1069
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 982 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant1 978 1  |-  ( ( ( ( ph  /\  ps )  /\  ch  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  pceu  13220  nllyrest  17549  exatleN  30201  2llnjaN  30363  2lplnja  30416  dalemceb  30435  pclfinN  30697  lhpexle3lem  30808  lhpmcvr5N  30824  lhpmcvr6N  30825  lhp2at0  30829  4atexlemw  30845  cdlemd2  30996  cdlemd4  30998  cdleme7aa  31039  cdleme7c  31042  cdleme7d  31043  cdleme7e  31044  cdleme7ga  31045  cdleme7  31046  cdleme15a  31071  cdleme15b  31072  cdleme15d  31074  cdleme15  31075  cdleme16b  31076  cdleme16c  31077  cdleme16d  31078  cdleme16e  31079  cdleme16f  31080  cdleme18d  31092  cdleme19b  31101  cdleme19d  31103  cdleme19e  31104  cdleme20d  31109  cdleme20e  31110  cdleme20f  31111  cdleme20g  31112  cdleme20h  31113  cdleme20j  31115  cdleme20k  31116  cdleme20l1  31117  cdleme20l2  31118  cdleme20l  31119  cdleme20m  31120  cdleme21c  31124  cdleme21ct  31126  cdleme22cN  31139  cdleme22f  31143  cdleme22g  31145  cdleme23a  31146  cdleme23b  31147  cdleme23c  31148  cdleme25a  31150  cdleme25c  31152  cdleme25dN  31153  cdleme26ee  31157  cdleme26eALTN  31158  cdleme27N  31166  cdleme28a  31167  cdleme28b  31168  cdleme29ex  31171  cdlemefr29exN  31199  cdleme32b  31239  cdleme32c  31240  cdleme32e  31242  cdleme35b  31247  cdleme35c  31248  cdleme35d  31249  cdleme35e  31250  cdleme35f  31251  cdleme42h  31279  cdleme42i  31280  cdleme42k  31281  cdleme48bw  31299  cdlemeg46frv  31322  cdlemeg46vrg  31324  cdlemeg46rgv  31325  cdlemeg46req  31326  cdlemf1  31358  trlord  31366  cdlemg7fvbwN  31404  cdlemg10  31438  cdlemg12e  31444  cdlemg12f  31445  cdlemg19a  31480  cdlemg31c  31496  cdlemg33c0  31499  cdlemg35  31510  tendococl  31569  cdlemh2  31613  cdlemh  31614  cdlemi  31617  cdlemk5  31633  cdlemk7  31645  cdlemk11  31646  cdlemk5u  31658  cdlemkj  31660  cdlemkuv2  31664  cdlemk7u  31667  cdlemk11u  31668  cdlemk26-3  31703  cdlemk11t  31743  cdlemk52  31751  cdlemk53a  31752  dihord1  32016  dihord2a  32017  dihord2b  32018  dihord11b  32020  dihord11c  32022  dihord2pre  32023  dihord2pre2  32024  dihord5apre  32060  dihmeetlem1N  32088  dihglblem2N  32092  dihglblem3N  32093  dihglbcpreN  32098  dihmeetlem3N  32103  dihjatc1  32109
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