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

Theorem simp2rl 1075
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 763 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant2 1028 1  |-  ( ( th  /\  ( ch 
/\  ( ph  /\  ps ) )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  tfrlem5  7104  omeu  7292  wemaplem3  8067  gruina  9245  4sqlem18OLD  14899  4sqlem18  14905  vdwlem10  14933  mdetuni0  19638  mdetmul  19640  tsmsxp  21161  ax5seglem3  24953  btwnconn1lem1  30853  btwnconn1lem2  30854  btwnconn1lem3  30855  btwnconn1lem4  30856  btwnconn1lem12  30864  btwnconn1lem13  30865  linethru  30919  2llnjN  33095  2lplnja  33147  2lplnj  33148  cdlemblem  33321  dalaw  33414  pclfinN  33428  lhpmcvr4N  33554  lhp2atne  33562  lhp2at0ne  33564  cdlemb2  33569  cdlemd7  33733  cdleme01N  33750  cdleme02N  33751  cdleme0ex2N  33753  cdleme7aa  33771  cdleme7c  33774  cdleme7d  33775  cdleme7e  33776  cdleme7ga  33777  cdleme11a  33789  cdleme20k  33849  cdleme21d  33860  cdleme27cl  33896  cdlemefrs29bpre0  33926  cdlemefrs29cpre1  33928  cdlemefrs32fva  33930  cdlemefrs32fva1  33931  cdlemefr29exN  33932  cdlemefr32sn2aw  33934  cdlemefr31fv1  33941  cdlemefs32sn1aw  33944  cdlemefr44  33955  cdlemefr45e  33958  cdleme41sn3a  33963  cdleme35a  33978  cdleme35fnpq  33979  cdleme35b  33980  cdleme35c  33981  cdleme35d  33982  cdleme35e  33983  cdleme35f  33984  cdleme35sn3a  33989  cdleme42e  34009  cdleme42h  34012  cdleme42i  34013  cdleme17d2  34025  cdleme48fv  34029  cdleme48bw  34032  cdleme48b  34033  cdlemeg46c  34043  cdlemeg46ngfr  34048  cdleme48d  34065  cdlemg2kq  34132  cdlemg2m  34134  cdlemg7fvN  34154  cdlemg8a  34157  cdlemg11aq  34168  cdlemg10c  34169  cdlemg17a  34191  cdlemg31b0N  34224  cdlemg41  34248  cdlemh2  34346  cdlemi  34350  cdlemk21-2N  34421  dihmeetlem1N  34821  dihmeetlem13N  34850  expmordi  35759  iunrelexpmin1  36204
  Copyright terms: Public domain W3C validator