Theorem simp2ll 1075

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 760	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> ph )
2	1	3ad2ant2 1030	1 |- ( ( th /\ ( ( ph /\ ps ) /\ ch ) /\ ta ) -> ph )

Syntax hints:   -> wi 4   /\ wa 371   /\ w3a 985

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 987

This theorem is referenced by:  tfrlem5  7098  omeu  7286  4sqlem18OLD  14906  4sqlem18  14912  vdwlem10  14940  0catg  15593  mvrf1  18649  mdetuni0  19646  mdetmul  19648  tsmsxp  21169  ax5seglem3  24961  btwnconn1lem1  30854  btwnconn1lem2  30855  btwnconn1lem3  30856  btwnconn1lem12  30865  btwnconn1lem13  30866  lshpkrlem6  32681  athgt  33021  2llnjN  33132  dalaw  33451  lhpmcvr4N  33591  cdlemb2  33606  4atexlemex6  33639  cdlemd7  33770  cdleme01N  33787  cdleme02N  33788  cdleme0ex1N  33789  cdleme0ex2N  33790  cdleme7aa  33808  cdleme7c  33811  cdleme7d  33812  cdleme7e  33813  cdleme7ga  33814  cdleme7  33815  cdleme11a  33826  cdleme20k  33886  cdleme27cl  33933  cdleme42e  34046  cdleme42h  34049  cdleme42i  34050  cdlemf  34130  cdlemg2kq  34169  cdlemg2m  34171  cdlemg8a  34194  cdlemg11aq  34205  cdlemg10c  34206  cdlemg11b  34209  cdlemg17a  34228  cdlemg31b0N  34261  cdlemg31c  34266  cdlemg33c0  34269  cdlemg41  34285  cdlemh2  34383  cdlemn9  34773  dihglbcpreN  34868  dihmeetlem3N  34873  dihmeetlem13N  34887  pellex  35679  expmordi  35795