Theorem simp2ll 1064

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

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

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 976

This theorem is referenced by:  tfrlem5  7051  omeu  7236  4sqlem18  14357  vdwlem10  14385  0catg  14961  mvrf1  17955  mdetuni0  18996  mdetmul  18998  tsmsxp  20530  ax5seglem3  24106  btwnconn1lem1  29712  btwnconn1lem2  29713  btwnconn1lem3  29714  btwnconn1lem12  29723  btwnconn1lem13  29724  pellex  30746  expmordi  30858  lshpkrlem6  34574  athgt  34914  2llnjN  35025  dalaw  35344  lhpmcvr4N  35484  cdlemb2  35499  4atexlemex6  35532  cdlemd7  35663  cdleme01N  35680  cdleme02N  35681  cdleme0ex1N  35682  cdleme0ex2N  35683  cdleme7aa  35701  cdleme7c  35704  cdleme7d  35705  cdleme7e  35706  cdleme7ga  35707  cdleme7  35708  cdleme11a  35719  cdleme20k  35779  cdleme27cl  35826  cdleme42e  35939  cdleme42h  35942  cdleme42i  35943  cdlemf  36023  cdlemg2kq  36062  cdlemg2m  36064  cdlemg8a  36087  cdlemg11aq  36098  cdlemg10c  36099  cdlemg11b  36102  cdlemg17a  36121  cdlemg31b0N  36154  cdlemg31c  36159  cdlemg33c0  36162  cdlemg41  36178  cdlemh2  36276  cdlemn9  36666  dihglbcpreN  36761  dihmeetlem3N  36766  dihmeetlem13N  36780