MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp2rl 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  6787  wemaplem3  7473  gruina  8649  4sqlem18  13285  vdwlem10  13313  tsmsxp  18137  ax5seglem3  25774  btwnconn1lem1  25925  btwnconn1lem2  25926  btwnconn1lem3  25927  btwnconn1lem4  25928  btwnconn1lem12  25936  btwnconn1lem13  25937  linethru  25991  expmordi  26900  2llnjN  30049  2lplnja  30101  2lplnj  30102  cdlemblem  30275  dalaw  30368  pclfinN  30382  lhpmcvr4N  30508  lhp2atne  30516  lhp2at0ne  30518  cdlemb2  30523  cdlemd7  30686  cdleme01N  30703  cdleme02N  30704  cdleme0ex2N  30706  cdleme7aa  30724  cdleme7c  30727  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme11a  30742  cdleme20k  30801  cdleme21d  30812  cdleme27cl  30848  cdlemefrs29bpre0  30878  cdlemefrs29cpre1  30880  cdlemefrs32fva  30882  cdlemefrs32fva1  30883  cdlemefr29exN  30884  cdlemefr32sn2aw  30886  cdlemefr31fv1  30893  cdlemefs32sn1aw  30896  cdlemefr44  30907  cdlemefr45e  30910  cdleme41sn3a  30915  cdleme35a  30930  cdleme35fnpq  30931  cdleme35b  30932  cdleme35c  30933  cdleme35d  30934  cdleme35e  30935  cdleme35f  30936  cdleme35sn3a  30941  cdleme42e  30961  cdleme42h  30964  cdleme42i  30965  cdleme17d2  30977  cdleme48fv  30981  cdleme48bw  30984  cdleme48b  30985  cdlemeg46c  30995  cdlemeg46ngfr  31000  cdleme48d  31017  cdlemg2kq  31084  cdlemg2m  31086  cdlemg7fvN  31106  cdlemg8a  31109  cdlemg11aq  31120  cdlemg10c  31121  cdlemg17a  31143  cdlemg31b0N  31176  cdlemg41  31200  cdlemh2  31298  cdlemi  31302  cdlemk21-2N  31373  dihmeetlem1N  31773  dihmeetlem13N  31802
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