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  6599  wemaplem3  7279  gruina  8456  4sqlem18  13025  vdwlem10  13053  tsmsxp  17853  ax5seglem3  24631  btwnconn1lem1  24782  btwnconn1lem2  24783  btwnconn1lem3  24784  btwnconn1lem4  24785  btwnconn1lem12  24793  btwnconn1lem13  24794  linethru  24848  expmordi  27135  2llnjN  30378  2lplnja  30430  2lplnj  30431  cdlemblem  30604  dalaw  30697  pclfinN  30711  lhpmcvr4N  30837  lhp2atne  30845  lhp2at0ne  30847  cdlemb2  30852  cdlemd7  31015  cdleme01N  31032  cdleme02N  31033  cdleme0ex2N  31035  cdleme7aa  31053  cdleme7c  31056  cdleme7d  31057  cdleme7e  31058  cdleme7ga  31059  cdleme11a  31071  cdleme20k  31130  cdleme21d  31141  cdleme27cl  31177  cdlemefrs29bpre0  31207  cdlemefrs29cpre1  31209  cdlemefrs32fva  31211  cdlemefrs32fva1  31212  cdlemefr29exN  31213  cdlemefr32sn2aw  31215  cdlemefr31fv1  31222  cdlemefs32sn1aw  31225  cdlemefr44  31236  cdlemefr45e  31239  cdleme41sn3a  31244  cdleme35a  31259  cdleme35fnpq  31260  cdleme35b  31261  cdleme35c  31262  cdleme35d  31263  cdleme35e  31264  cdleme35f  31265  cdleme35sn3a  31270  cdleme42e  31290  cdleme42h  31293  cdleme42i  31294  cdleme17d2  31306  cdleme48fv  31310  cdleme48bw  31313  cdleme48b  31314  cdlemeg46c  31324  cdlemeg46ngfr  31329  cdleme48d  31346  cdlemg2kq  31413  cdlemg2m  31415  cdlemg7fvN  31435  cdlemg8a  31438  cdlemg11aq  31449  cdlemg10c  31450  cdlemg17a  31472  cdlemg31b0N  31505  cdlemg41  31529  cdlemh2  31627  cdlemi  31631  cdlemk21-2N  31702  dihmeetlem1N  32102  dihmeetlem13N  32131
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