Theorem simp2ll 1055

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

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965

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 185  df-an 371  df-3an 967

This theorem is referenced by:  tfrlem5  6839  omeu  7024  4sqlem18  14023  vdwlem10  14051  0catg  14625  mvrf1  17498  mdetuni0  18427  mdetmul  18429  tsmsxp  19729  ax5seglem3  23177  btwnconn1lem1  28118  btwnconn1lem2  28119  btwnconn1lem3  28120  btwnconn1lem12  28129  btwnconn1lem13  28130  pellex  29176  expmordi  29288  lshpkrlem6  32760  athgt  33100  2llnjN  33211  dalaw  33530  lhpmcvr4N  33670  cdlemb2  33685  4atexlemex6  33718  cdlemd7  33848  cdleme01N  33865  cdleme02N  33866  cdleme0ex1N  33867  cdleme0ex2N  33868  cdleme7aa  33886  cdleme7c  33889  cdleme7d  33890  cdleme7e  33891  cdleme7ga  33892  cdleme7  33893  cdleme11a  33904  cdleme20k  33963  cdleme27cl  34010  cdleme42e  34123  cdleme42h  34126  cdleme42i  34127  cdlemf  34207  cdlemg2kq  34246  cdlemg2m  34248  cdlemg8a  34271  cdlemg11aq  34282  cdlemg10c  34283  cdlemg11b  34286  cdlemg17a  34305  cdlemg31b0N  34338  cdlemg31c  34343  cdlemg33c0  34346  cdlemg41  34362  cdlemh2  34460  cdlemn9  34850  dihglbcpreN  34945  dihmeetlem3N  34950  dihmeetlem13N  34964