Theorem simp13l 1289

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

Assertion

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

Proof of Theorem simp13l

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

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

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 1088

This theorem is referenced by:  pceu  16817  axpasch  28868  3atlem4  39480  llncvrlpln2  39551  2lplnja  39613  2lnat  39778  llnexchb2  39863  lhp2lt  39995  lhpmcvr5N  40021  4atexlemq  40045  4atexlemex6  40068  trlval2  40157  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme11l  40263  cdleme11  40264  cdleme14  40267  cdleme15a  40268  cdleme15b  40269  cdleme15  40272  cdleme16b  40273  cdleme16c  40274  cdleme16d  40275  cdleme18d  40289  cdleme19b  40298  cdleme19e  40301  cdleme20d  40306  cdleme20g  40309  cdleme20h  40310  cdleme20i  40311  cdleme20j  40312  cdleme20l2  40315  cdleme20l  40316  cdleme20m  40317  cdleme21d  40324  cdleme21e  40325  cdleme21h  40328  cdleme22f  40340  cdleme23a  40343  cdleme23b  40344  cdleme23c  40345  cdleme24  40346  cdleme25a  40347  cdleme25dN  40350  cdleme26ee  40354  cdleme26fALTN  40356  cdleme26f  40357  cdleme26f2ALTN  40358  cdleme26f2  40359  cdleme27a  40361  cdlemefr29bpre0N  40400  cdlemefr29clN  40401  cdlemefr32fvaN  40403  cdlemefr32fva1  40404  cdleme41sn3a  40427  cdleme35a  40442  cdleme35fnpq  40443  cdleme35b  40444  cdleme35c  40445  cdleme35d  40446  cdleme35f  40448  cdleme36m  40455  cdleme37m  40456  cdleme39n  40460  cdleme43bN  40484  cdleme43dN  40486  cdleme17d2  40489  cdlemeg46c  40507  cdlemeg46nlpq  40511  cdlemeg46ngfr  40512  cdlemeg46req  40523  cdlemeg46gfv  40524  cdleme50trn1  40543  cdleme50trn2a  40544  cdlemf1  40555  cdlemf  40557  cdlemg10a  40634  cdlemg10  40635  cdlemg12d  40640  cdlemg12e  40641  cdlemg12f  40642  cdlemg12g  40643  cdlemg12  40644  cdlemg13  40646  cdlemg16ALTN  40652  cdlemg17b  40656  cdlemg17h  40662  cdlemg17pq  40666  cdlemg17iqN  40668  cdlemg17  40671  cdlemg19a  40677  cdlemg19  40678  cdlemg21  40680  cdlemg27a  40686  cdlemg27b  40690  cdlemg31c  40693  cdlemg33b0  40695  cdlemg33a  40700  cdlemg48  40731  tendocan  40818  cdlemk26-3  40900  cdlemk27-3  40901  cdlemk28-3  40902  cdlemk37  40908  cdlemky  40920  cdlemkyu  40921  cdlemk11ta  40923  cdlemkid3N  40927  cdlemk42  40935  cdlemk42yN  40938  cdlemk11t  40940  cdlemk45  40941  cdlemk46  40942  cdlemk47  40943  cdlemk51  40947  cdlemk52  40948  cdlemk53a  40949  cdleml4N  40973  dihord2pre2  41220  dihord4  41252  dihord5apre  41256  dihmeetlem1N  41284  dihmeetlem15N  41315  mapdpglem32  41699  mzpcong  42961  mullimc  45614  mullimcf  45621  addlimc  45646  iscnrm3rlem8  48935