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

Theorem simp2rl 1066
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 756 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant2 1019 1  |-  ( ( th  /\  ( ch 
/\  ( ph  /\  ps ) )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976
This theorem is referenced by:  tfrlem5  7051  omeu  7236  wemaplem3  7976  gruina  9199  4sqlem18  14462  vdwlem10  14490  mdetuni0  19101  mdetmul  19103  tsmsxp  20635  ax5seglem3  24212  btwnconn1lem1  29713  btwnconn1lem2  29714  btwnconn1lem3  29715  btwnconn1lem4  29716  btwnconn1lem12  29724  btwnconn1lem13  29725  linethru  29779  expmordi  30859  2llnjN  35166  2lplnja  35218  2lplnj  35219  cdlemblem  35392  dalaw  35485  pclfinN  35499  lhpmcvr4N  35625  lhp2atne  35633  lhp2at0ne  35635  cdlemb2  35640  cdlemd7  35804  cdleme01N  35821  cdleme02N  35822  cdleme0ex2N  35824  cdleme7aa  35842  cdleme7c  35845  cdleme7d  35846  cdleme7e  35847  cdleme7ga  35848  cdleme11a  35860  cdleme20k  35920  cdleme21d  35931  cdleme27cl  35967  cdlemefrs29bpre0  35997  cdlemefrs29cpre1  35999  cdlemefrs32fva  36001  cdlemefrs32fva1  36002  cdlemefr29exN  36003  cdlemefr32sn2aw  36005  cdlemefr31fv1  36012  cdlemefs32sn1aw  36015  cdlemefr44  36026  cdlemefr45e  36029  cdleme41sn3a  36034  cdleme35a  36049  cdleme35fnpq  36050  cdleme35b  36051  cdleme35c  36052  cdleme35d  36053  cdleme35e  36054  cdleme35f  36055  cdleme35sn3a  36060  cdleme42e  36080  cdleme42h  36083  cdleme42i  36084  cdleme17d2  36096  cdleme48fv  36100  cdleme48bw  36103  cdleme48b  36104  cdlemeg46c  36114  cdlemeg46ngfr  36119  cdleme48d  36136  cdlemg2kq  36203  cdlemg2m  36205  cdlemg7fvN  36225  cdlemg8a  36228  cdlemg11aq  36239  cdlemg10c  36240  cdlemg17a  36262  cdlemg31b0N  36295  cdlemg41  36319  cdlemh2  36417  cdlemi  36421  cdlemk21-2N  36492  dihmeetlem1N  36892  dihmeetlem13N  36921
  Copyright terms: Public domain W3C validator