Theorem simp13l 1176

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp13l	|- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta /\ et ) -> ph )

Proof of Theorem simp13l

Step	Hyp	Ref	Expression
1		simp3l 1089	. 2 |- ( ( ch /\ th /\ ( ph /\ ps ) ) -> ph )
2	1	3ad2ant1 1082	1 |- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta /\ et ) -> ph )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  pceu  15551  axpasch  25821  3atlem4  34772  llncvrlpln2  34843  2lplnja  34905  2lnat  35070  llnexchb2  35155  lhp2lt  35287  lhpmcvr5N  35313  4atexlemq  35337  4atexlemex6  35360  trlval2  35450  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme11l  35556  cdleme11  35557  cdleme14  35560  cdleme15a  35561  cdleme15b  35562  cdleme15  35565  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme18d  35582  cdleme19b  35592  cdleme19e  35595  cdleme20d  35600  cdleme20g  35603  cdleme20h  35604  cdleme20i  35605  cdleme20j  35606  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme21d  35618  cdleme21e  35619  cdleme21h  35622  cdleme22f  35634  cdleme23a  35637  cdleme23b  35638  cdleme23c  35639  cdleme24  35640  cdleme25a  35641  cdleme25dN  35644  cdleme26ee  35648  cdleme26fALTN  35650  cdleme26f  35651  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme27a  35655  cdlemefr29bpre0N  35694  cdlemefr29clN  35695  cdlemefr32fvaN  35697  cdlemefr32fva1  35698  cdleme41sn3a  35721  cdleme35a  35736  cdleme35fnpq  35737  cdleme35b  35738  cdleme35c  35739  cdleme35d  35740  cdleme35f  35742  cdleme36m  35749  cdleme37m  35750  cdleme39n  35754  cdleme43bN  35778  cdleme43dN  35780  cdleme17d2  35783  cdlemeg46c  35801  cdlemeg46nlpq  35805  cdlemeg46ngfr  35806  cdlemeg46req  35817  cdlemeg46gfv  35818  cdleme50trn1  35837  cdleme50trn2a  35838  cdlemf1  35849  cdlemf  35851  cdlemg10a  35928  cdlemg10  35929  cdlemg12d  35934  cdlemg12e  35935  cdlemg12f  35936  cdlemg12g  35937  cdlemg12  35938  cdlemg13  35940  cdlemg16ALTN  35946  cdlemg17b  35950  cdlemg17h  35956  cdlemg17pq  35960  cdlemg17iqN  35962  cdlemg17  35965  cdlemg19a  35971  cdlemg19  35972  cdlemg21  35974  cdlemg27a  35980  cdlemg27b  35984  cdlemg31c  35987  cdlemg33b0  35989  cdlemg33a  35994  cdlemg48  36025  tendocan  36112  cdlemk26-3  36194  cdlemk27-3  36195  cdlemk28-3  36196  cdlemk37  36202  cdlemky  36214  cdlemkyu  36215  cdlemk11ta  36217  cdlemkid3N  36221  cdlemk42  36229  cdlemk42yN  36232  cdlemk11t  36234  cdlemk45  36235  cdlemk46  36236  cdlemk47  36237  cdlemk51  36241  cdlemk52  36242  cdlemk53a  36243  cdleml4N  36267  dihord2pre2  36515  dihord4  36547  dihord5apre  36551  dihmeetlem1N  36579  dihmeetlem15N  36610  mapdpglem32  36994  mzpcong  37539  mullimc  39848  mullimcf  39855  addlimc  39880