Theorem simp2rl 1130

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp2rl	|- ( ( th /\ ( ch /\ ( ph /\ ps ) ) /\ ta ) -> ph )

Proof of Theorem simp2rl

Step	Hyp	Ref	Expression
1		simprl 794	. 2 |- ( ( ch /\ ( ph /\ ps ) ) -> ph )
2	1	3ad2ant2 1083	1 |- ( ( th /\ ( ch /\ ( ph /\ ps ) ) /\ ta ) -> ph )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  tfrlem5  7476  omeu  7665  wemaplem3  8453  gruina  9640  4sqlem18  15666  vdwlem10  15694  mdetuni0  20427  mdetmul  20429  tsmsxp  21958  ax5seglem3  25811  btwnconn1lem1  32194  btwnconn1lem2  32195  btwnconn1lem3  32196  btwnconn1lem4  32197  btwnconn1lem12  32205  btwnconn1lem13  32206  linethru  32260  2llnjN  34853  2lplnja  34905  2lplnj  34906  cdlemblem  35079  dalaw  35172  pclfinN  35186  lhpmcvr4N  35312  lhp2atne  35320  lhp2at0ne  35322  cdlemb2  35327  cdlemd7  35491  cdleme01N  35508  cdleme02N  35509  cdleme0ex2N  35511  cdleme7aa  35529  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme11a  35547  cdleme20k  35607  cdleme21d  35618  cdleme27cl  35654  cdlemefrs29bpre0  35684  cdlemefrs29cpre1  35686  cdlemefrs32fva  35688  cdlemefrs32fva1  35689  cdlemefr29exN  35690  cdlemefr32sn2aw  35692  cdlemefr31fv1  35699  cdlemefs32sn1aw  35702  cdlemefr44  35713  cdlemefr45e  35716  cdleme41sn3a  35721  cdleme35a  35736  cdleme35fnpq  35737  cdleme35b  35738  cdleme35c  35739  cdleme35d  35740  cdleme35e  35741  cdleme35f  35742  cdleme35sn3a  35747  cdleme42e  35767  cdleme42h  35770  cdleme42i  35771  cdleme17d2  35783  cdleme48fv  35787  cdleme48bw  35790  cdleme48b  35791  cdlemeg46c  35801  cdlemeg46ngfr  35806  cdleme48d  35823  cdlemg2kq  35890  cdlemg2m  35892  cdlemg7fvN  35912  cdlemg8a  35915  cdlemg11aq  35926  cdlemg10c  35927  cdlemg17a  35949  cdlemg31b0N  35982  cdlemg41  36006  cdlemh2  36104  cdlemi  36108  cdlemk21-2N  36179  dihmeetlem1N  36579  dihmeetlem13N  36608  expmordi  37512  iunrelexpmin1  38000