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

Theorem simp2rl 1024
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp2rl  |-  ( ( th  /\  ( ch 
/\  ( ph  /\  ps ) )  /\  ta )  ->  ph )

Proof of Theorem simp2rl
StepHypRef Expression
1 simprl 732 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant2 977 1  |-  ( ( th  /\  ( ch 
/\  ( ph  /\  ps ) )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  omeu  6583  wemaplem3  7263  gruina  8440  4sqlem18  13009  vdwlem10  13037  tsmsxp  17837  ax5seglem3  24559  btwnconn1lem1  24710  btwnconn1lem2  24711  btwnconn1lem3  24712  btwnconn1lem4  24713  btwnconn1lem12  24721  btwnconn1lem13  24722  linethru  24776  expmordi  27032  2llnjN  29756  2lplnja  29808  2lplnj  29809  cdlemblem  29982  dalaw  30075  pclfinN  30089  lhpmcvr4N  30215  lhp2atne  30223  lhp2at0ne  30225  cdlemb2  30230  cdlemd7  30393  cdleme01N  30410  cdleme02N  30411  cdleme0ex2N  30413  cdleme7aa  30431  cdleme7c  30434  cdleme7d  30435  cdleme7e  30436  cdleme7ga  30437  cdleme11a  30449  cdleme20k  30508  cdleme21d  30519  cdleme27cl  30555  cdlemefrs29bpre0  30585  cdlemefrs29cpre1  30587  cdlemefrs32fva  30589  cdlemefrs32fva1  30590  cdlemefr29exN  30591  cdlemefr32sn2aw  30593  cdlemefr31fv1  30600  cdlemefs32sn1aw  30603  cdlemefr44  30614  cdlemefr45e  30617  cdleme41sn3a  30622  cdleme35a  30637  cdleme35fnpq  30638  cdleme35b  30639  cdleme35c  30640  cdleme35d  30641  cdleme35e  30642  cdleme35f  30643  cdleme35sn3a  30648  cdleme42e  30668  cdleme42h  30671  cdleme42i  30672  cdleme17d2  30684  cdleme48fv  30688  cdleme48bw  30691  cdleme48b  30692  cdlemeg46c  30702  cdlemeg46ngfr  30707  cdleme48d  30724  cdlemg2kq  30791  cdlemg2m  30793  cdlemg7fvN  30813  cdlemg8a  30816  cdlemg11aq  30827  cdlemg10c  30828  cdlemg17a  30850  cdlemg31b0N  30883  cdlemg41  30907  cdlemh2  31005  cdlemi  31009  cdlemk21-2N  31080  dihmeetlem1N  31480  dihmeetlem13N  31509
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