Theorem simp13l 1290

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

Assertion

Ref	Expression
simp13l	⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Proof of Theorem simp13l

Step	Hyp	Ref	Expression
1		simp3l 1203	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2ant1 1134	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  pceu  16808  axpasch  29024  3atlem4  39946  llncvrlpln2  40017  2lplnja  40079  2lnat  40244  llnexchb2  40329  lhp2lt  40461  lhpmcvr5N  40487  4atexlemq  40511  4atexlemex6  40534  trlval2  40623  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme7  40709  cdleme11l  40729  cdleme11  40730  cdleme14  40733  cdleme15a  40734  cdleme15b  40735  cdleme15  40738  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme18d  40755  cdleme19b  40764  cdleme19e  40767  cdleme20d  40772  cdleme20g  40775  cdleme20h  40776  cdleme20i  40777  cdleme20j  40778  cdleme20l2  40781  cdleme20l  40782  cdleme20m  40783  cdleme21d  40790  cdleme21e  40791  cdleme21h  40794  cdleme22f  40806  cdleme23a  40809  cdleme23b  40810  cdleme23c  40811  cdleme24  40812  cdleme25a  40813  cdleme25dN  40816  cdleme26ee  40820  cdleme26fALTN  40822  cdleme26f  40823  cdleme26f2ALTN  40824  cdleme26f2  40825  cdleme27a  40827  cdlemefr29bpre0N  40866  cdlemefr29clN  40867  cdlemefr32fvaN  40869  cdlemefr32fva1  40870  cdleme41sn3a  40893  cdleme35a  40908  cdleme35fnpq  40909  cdleme35b  40910  cdleme35c  40911  cdleme35d  40912  cdleme35f  40914  cdleme36m  40921  cdleme37m  40922  cdleme39n  40926  cdleme43bN  40950  cdleme43dN  40952  cdleme17d2  40955  cdlemeg46c  40973  cdlemeg46nlpq  40977  cdlemeg46ngfr  40978  cdlemeg46req  40989  cdlemeg46gfv  40990  cdleme50trn1  41009  cdleme50trn2a  41010  cdlemf1  41021  cdlemf  41023  cdlemg10a  41100  cdlemg10  41101  cdlemg12d  41106  cdlemg12e  41107  cdlemg12f  41108  cdlemg12g  41109  cdlemg12  41110  cdlemg13  41112  cdlemg16ALTN  41118  cdlemg17b  41122  cdlemg17h  41128  cdlemg17pq  41132  cdlemg17iqN  41134  cdlemg17  41137  cdlemg19a  41143  cdlemg19  41144  cdlemg21  41146  cdlemg27a  41152  cdlemg27b  41156  cdlemg31c  41159  cdlemg33b0  41161  cdlemg33a  41166  cdlemg48  41197  tendocan  41284  cdlemk26-3  41366  cdlemk27-3  41367  cdlemk28-3  41368  cdlemk37  41374  cdlemky  41386  cdlemkyu  41387  cdlemk11ta  41389  cdlemkid3N  41393  cdlemk42  41401  cdlemk42yN  41404  cdlemk11t  41406  cdlemk45  41407  cdlemk46  41408  cdlemk47  41409  cdlemk51  41413  cdlemk52  41414  cdlemk53a  41415  cdleml4N  41439  dihord2pre2  41686  dihord4  41718  dihord5apre  41722  dihmeetlem1N  41750  dihmeetlem15N  41781  mapdpglem32  42165  mzpcong  43418  mullimc  46064  mullimcf  46071  addlimc  46094  iscnrm3rlem8  49434