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

Theorem simp2rl 1063
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 754 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant2 1016 1  |-  ( ( th  /\  ( ch 
/\  ( ph  /\  ps ) )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  tfrlem5  6967  omeu  7152  wemaplem3  7888  gruina  9107  4sqlem18  14482  vdwlem10  14510  mdetuni0  19208  mdetmul  19210  tsmsxp  20742  ax5seglem3  24355  btwnconn1lem1  29890  btwnconn1lem2  29891  btwnconn1lem3  29892  btwnconn1lem4  29893  btwnconn1lem12  29901  btwnconn1lem13  29902  linethru  29956  expmordi  31048  2llnjN  35704  2lplnja  35756  2lplnj  35757  cdlemblem  35930  dalaw  36023  pclfinN  36037  lhpmcvr4N  36163  lhp2atne  36171  lhp2at0ne  36173  cdlemb2  36178  cdlemd7  36342  cdleme01N  36359  cdleme02N  36360  cdleme0ex2N  36362  cdleme7aa  36380  cdleme7c  36383  cdleme7d  36384  cdleme7e  36385  cdleme7ga  36386  cdleme11a  36398  cdleme20k  36458  cdleme21d  36469  cdleme27cl  36505  cdlemefrs29bpre0  36535  cdlemefrs29cpre1  36537  cdlemefrs32fva  36539  cdlemefrs32fva1  36540  cdlemefr29exN  36541  cdlemefr32sn2aw  36543  cdlemefr31fv1  36550  cdlemefs32sn1aw  36553  cdlemefr44  36564  cdlemefr45e  36567  cdleme41sn3a  36572  cdleme35a  36587  cdleme35fnpq  36588  cdleme35b  36589  cdleme35c  36590  cdleme35d  36591  cdleme35e  36592  cdleme35f  36593  cdleme35sn3a  36598  cdleme42e  36618  cdleme42h  36621  cdleme42i  36622  cdleme17d2  36634  cdleme48fv  36638  cdleme48bw  36641  cdleme48b  36642  cdlemeg46c  36652  cdlemeg46ngfr  36657  cdleme48d  36674  cdlemg2kq  36741  cdlemg2m  36743  cdlemg7fvN  36763  cdlemg8a  36766  cdlemg11aq  36777  cdlemg10c  36778  cdlemg17a  36800  cdlemg31b0N  36833  cdlemg41  36857  cdlemh2  36955  cdlemi  36959  cdlemk21-2N  37030  dihmeetlem1N  37430  dihmeetlem13N  37459  iunrelexpmin1  38225
  Copyright terms: Public domain W3C validator