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

Theorem simp2rl 1078
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 765 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps ) )  ->  ph )
213ad2ant2 1031 1  |-  ( ( th  /\  ( ch 
/\  ( ph  /\  ps ) )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 986
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 988
This theorem is referenced by:  tfrlem5  7103  omeu  7291  wemaplem3  8068  gruina  9248  4sqlem18OLD  14918  4sqlem18  14924  vdwlem10  14952  mdetuni0  19658  mdetmul  19660  tsmsxp  21181  ax5seglem3  24973  btwnconn1lem1  30866  btwnconn1lem2  30867  btwnconn1lem3  30868  btwnconn1lem4  30869  btwnconn1lem12  30877  btwnconn1lem13  30878  linethru  30932  2llnjN  33144  2lplnja  33196  2lplnj  33197  cdlemblem  33370  dalaw  33463  pclfinN  33477  lhpmcvr4N  33603  lhp2atne  33611  lhp2at0ne  33613  cdlemb2  33618  cdlemd7  33782  cdleme01N  33799  cdleme02N  33800  cdleme0ex2N  33802  cdleme7aa  33820  cdleme7c  33823  cdleme7d  33824  cdleme7e  33825  cdleme7ga  33826  cdleme11a  33838  cdleme20k  33898  cdleme21d  33909  cdleme27cl  33945  cdlemefrs29bpre0  33975  cdlemefrs29cpre1  33977  cdlemefrs32fva  33979  cdlemefrs32fva1  33980  cdlemefr29exN  33981  cdlemefr32sn2aw  33983  cdlemefr31fv1  33990  cdlemefs32sn1aw  33993  cdlemefr44  34004  cdlemefr45e  34007  cdleme41sn3a  34012  cdleme35a  34027  cdleme35fnpq  34028  cdleme35b  34029  cdleme35c  34030  cdleme35d  34031  cdleme35e  34032  cdleme35f  34033  cdleme35sn3a  34038  cdleme42e  34058  cdleme42h  34061  cdleme42i  34062  cdleme17d2  34074  cdleme48fv  34078  cdleme48bw  34081  cdleme48b  34082  cdlemeg46c  34092  cdlemeg46ngfr  34097  cdleme48d  34114  cdlemg2kq  34181  cdlemg2m  34183  cdlemg7fvN  34203  cdlemg8a  34206  cdlemg11aq  34217  cdlemg10c  34218  cdlemg17a  34240  cdlemg31b0N  34273  cdlemg41  34297  cdlemh2  34395  cdlemi  34399  cdlemk21-2N  34470  dihmeetlem1N  34870  dihmeetlem13N  34899  expmordi  35807  iunrelexpmin1  36312
  Copyright terms: Public domain W3C validator