MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp11r 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  13179  nllyrest  17506  exatleN  29890  2llnjaN  30052  2lplnja  30105  dalemceb  30124  pclfinN  30386  lhpexle3lem  30497  lhpmcvr5N  30513  lhpmcvr6N  30514  lhp2at0  30518  4atexlemw  30534  cdlemd2  30685  cdlemd4  30687  cdleme7aa  30728  cdleme7c  30731  cdleme7d  30732  cdleme7e  30733  cdleme7ga  30734  cdleme7  30735  cdleme15a  30760  cdleme15b  30761  cdleme15d  30763  cdleme15  30764  cdleme16b  30765  cdleme16c  30766  cdleme16d  30767  cdleme16e  30768  cdleme16f  30769  cdleme18d  30781  cdleme19b  30790  cdleme19d  30792  cdleme19e  30793  cdleme20d  30798  cdleme20e  30799  cdleme20f  30800  cdleme20g  30801  cdleme20h  30802  cdleme20j  30804  cdleme20k  30805  cdleme20l1  30806  cdleme20l2  30807  cdleme20l  30808  cdleme20m  30809  cdleme21c  30813  cdleme21ct  30815  cdleme22cN  30828  cdleme22f  30832  cdleme22g  30834  cdleme23a  30835  cdleme23b  30836  cdleme23c  30837  cdleme25a  30839  cdleme25c  30841  cdleme25dN  30842  cdleme26ee  30846  cdleme26eALTN  30847  cdleme27N  30855  cdleme28a  30856  cdleme28b  30857  cdleme29ex  30860  cdlemefr29exN  30888  cdleme32b  30928  cdleme32c  30929  cdleme32e  30931  cdleme35b  30936  cdleme35c  30937  cdleme35d  30938  cdleme35e  30939  cdleme35f  30940  cdleme42h  30968  cdleme42i  30969  cdleme42k  30970  cdleme48bw  30988  cdlemeg46frv  31011  cdlemeg46vrg  31013  cdlemeg46rgv  31014  cdlemeg46req  31015  cdlemf1  31047  trlord  31055  cdlemg7fvbwN  31093  cdlemg10  31127  cdlemg12e  31133  cdlemg12f  31134  cdlemg19a  31169  cdlemg31c  31185  cdlemg33c0  31188  cdlemg35  31199  tendococl  31258  cdlemh2  31302  cdlemh  31303  cdlemi  31306  cdlemk5  31322  cdlemk7  31334  cdlemk11  31335  cdlemk5u  31347  cdlemkj  31349  cdlemkuv2  31353  cdlemk7u  31356  cdlemk11u  31357  cdlemk26-3  31392  cdlemk11t  31432  cdlemk52  31440  cdlemk53a  31441  dihord1  31705  dihord2a  31706  dihord2b  31707  dihord11b  31709  dihord11c  31711  dihord2pre  31712  dihord2pre2  31713  dihord5apre  31749  dihmeetlem1N  31777  dihglblem2N  31781  dihglblem3N  31782  dihglbcpreN  31787  dihmeetlem3N  31792  dihjatc1  31798
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