Theorem simp2ll 1072

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

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982

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 188  df-an 372  df-3an 984

This theorem is referenced by:  tfrlem5  7103  omeu  7291  4sqlem18OLD  14894  4sqlem18  14900  vdwlem10  14928  0catg  15581  mvrf1  18637  mdetuni0  19633  mdetmul  19635  tsmsxp  21156  ax5seglem3  24948  btwnconn1lem1  30847  btwnconn1lem2  30848  btwnconn1lem3  30849  btwnconn1lem12  30858  btwnconn1lem13  30859  lshpkrlem6  32600  athgt  32940  2llnjN  33051  dalaw  33370  lhpmcvr4N  33510  cdlemb2  33525  4atexlemex6  33558  cdlemd7  33689  cdleme01N  33706  cdleme02N  33707  cdleme0ex1N  33708  cdleme0ex2N  33709  cdleme7aa  33727  cdleme7c  33730  cdleme7d  33731  cdleme7e  33732  cdleme7ga  33733  cdleme7  33734  cdleme11a  33745  cdleme20k  33805  cdleme27cl  33852  cdleme42e  33965  cdleme42h  33968  cdleme42i  33969  cdlemf  34049  cdlemg2kq  34088  cdlemg2m  34090  cdlemg8a  34113  cdlemg11aq  34124  cdlemg10c  34125  cdlemg11b  34128  cdlemg17a  34147  cdlemg31b0N  34180  cdlemg31c  34185  cdlemg33c0  34188  cdlemg41  34204  cdlemh2  34302  cdlemn9  34692  dihglbcpreN  34787  dihmeetlem3N  34792  dihmeetlem13N  34806  pellex  35599  expmordi  35715