Theorem simp2ll 1063

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 1018	1 |- ( ( th /\ ( ( ph /\ ps ) /\ ch ) /\ ta ) -> ph )

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

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 975

This theorem is referenced by:  tfrlem5  7049  omeu  7234  4sqlem18  14338  vdwlem10  14366  0catg  14941  mvrf1  17868  mdetuni0  18906  mdetmul  18908  tsmsxp  20408  ax5seglem3  23926  btwnconn1lem1  29330  btwnconn1lem2  29331  btwnconn1lem3  29332  btwnconn1lem12  29341  btwnconn1lem13  29342  pellex  30391  expmordi  30503  lshpkrlem6  33921  athgt  34261  2llnjN  34372  dalaw  34691  lhpmcvr4N  34831  cdlemb2  34846  4atexlemex6  34879  cdlemd7  35009  cdleme01N  35026  cdleme02N  35027  cdleme0ex1N  35028  cdleme0ex2N  35029  cdleme7aa  35047  cdleme7c  35050  cdleme7d  35051  cdleme7e  35052  cdleme7ga  35053  cdleme7  35054  cdleme11a  35065  cdleme20k  35124  cdleme27cl  35171  cdleme42e  35284  cdleme42h  35287  cdleme42i  35288  cdlemf  35368  cdlemg2kq  35407  cdlemg2m  35409  cdlemg8a  35432  cdlemg11aq  35443  cdlemg10c  35444  cdlemg11b  35447  cdlemg17a  35466  cdlemg31b0N  35499  cdlemg31c  35504  cdlemg33c0  35507  cdlemg41  35523  cdlemh2  35621  cdlemn9  36011  dihglbcpreN  36106  dihmeetlem3N  36111  dihmeetlem13N  36125