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

Theorem simp2rl 1026
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 733 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant2 979 1  |-  ( ( th  /\  ( ch 
/\  ( ph  /\  ps ) )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  omeu  6828  wemaplem3  7517  gruina  8693  4sqlem18  13330  vdwlem10  13358  tsmsxp  18184  ax5seglem3  25870  btwnconn1lem1  26021  btwnconn1lem2  26022  btwnconn1lem3  26023  btwnconn1lem4  26024  btwnconn1lem12  26032  btwnconn1lem13  26033  linethru  26087  expmordi  27010  2llnjN  30364  2lplnja  30416  2lplnj  30417  cdlemblem  30590  dalaw  30683  pclfinN  30697  lhpmcvr4N  30823  lhp2atne  30831  lhp2at0ne  30833  cdlemb2  30838  cdlemd7  31001  cdleme01N  31018  cdleme02N  31019  cdleme0ex2N  31021  cdleme7aa  31039  cdleme7c  31042  cdleme7d  31043  cdleme7e  31044  cdleme7ga  31045  cdleme11a  31057  cdleme20k  31116  cdleme21d  31127  cdleme27cl  31163  cdlemefrs29bpre0  31193  cdlemefrs29cpre1  31195  cdlemefrs32fva  31197  cdlemefrs32fva1  31198  cdlemefr29exN  31199  cdlemefr32sn2aw  31201  cdlemefr31fv1  31208  cdlemefs32sn1aw  31211  cdlemefr44  31222  cdlemefr45e  31225  cdleme41sn3a  31230  cdleme35a  31245  cdleme35fnpq  31246  cdleme35b  31247  cdleme35c  31248  cdleme35d  31249  cdleme35e  31250  cdleme35f  31251  cdleme35sn3a  31256  cdleme42e  31276  cdleme42h  31279  cdleme42i  31280  cdleme17d2  31292  cdleme48fv  31296  cdleme48bw  31299  cdleme48b  31300  cdlemeg46c  31310  cdlemeg46ngfr  31315  cdleme48d  31332  cdlemg2kq  31399  cdlemg2m  31401  cdlemg7fvN  31421  cdlemg8a  31424  cdlemg11aq  31435  cdlemg10c  31436  cdlemg17a  31458  cdlemg31b0N  31491  cdlemg41  31515  cdlemh2  31613  cdlemi  31617  cdlemk21-2N  31688  dihmeetlem1N  32088  dihmeetlem13N  32117
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