Theorem simp2ll 1128

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

Assertion

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

Proof of Theorem simp2ll

Step	Hyp	Ref	Expression
1		simpll 790	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ph )
2	1	3ad2ant2 1083	1 |- ( ( th /\ ( ( ph /\ ps ) /\ ch ) /\ 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  4sqlem18  15666  vdwlem10  15694  0catg  16348  mvrf1  19425  mdetuni0  20427  mdetmul  20429  tsmsxp  21958  ax5seglem3  25811  btwnconn1lem1  32194  btwnconn1lem2  32195  btwnconn1lem3  32196  btwnconn1lem12  32205  btwnconn1lem13  32206  lshpkrlem6  34402  athgt  34742  2llnjN  34853  dalaw  35172  lhpmcvr4N  35312  cdlemb2  35327  4atexlemex6  35360  cdlemd7  35491  cdleme01N  35508  cdleme02N  35509  cdleme0ex1N  35510  cdleme0ex2N  35511  cdleme7aa  35529  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme11a  35547  cdleme20k  35607  cdleme27cl  35654  cdleme42e  35767  cdleme42h  35770  cdleme42i  35771  cdlemf  35851  cdlemg2kq  35890  cdlemg2m  35892  cdlemg8a  35915  cdlemg11aq  35926  cdlemg10c  35927  cdlemg11b  35930  cdlemg17a  35949  cdlemg31b0N  35982  cdlemg31c  35987  cdlemg33c0  35990  cdlemg41  36006  cdlemh2  36104  cdlemn9  36494  dihglbcpreN  36589  dihmeetlem3N  36594  dihmeetlem13N  36608  pellex  37399  expmordi  37512