Theorem simp12l 1287

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

Assertion

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

Proof of Theorem simp12l

Step	Hyp	Ref	Expression
1		simp2l 1200	. 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:  ackbij1lem16  10187  axcontlem4  28894  eqlkr  39092  athgt  39450  llncvrlpln2  39551  4atlem11b  39602  2lnat  39778  cdlemblem  39787  pclfinN  39894  lhp2lt  39995  lhpmcvr5N  40021  lhpmcvr6N  40022  lhp2at0  40026  lhp2atnle  40027  lhp2at0nle  40029  4atexlemex6  40068  cdlemd2  40193  cdlemd7  40198  cdlemd8  40199  cdlemd9  40200  cdleme7aa  40236  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme11c  40255  cdleme11dN  40256  cdleme11e  40257  cdleme11  40264  cdleme14  40267  cdleme15a  40268  cdleme15b  40269  cdleme15d  40271  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  cdleme21c  40321  cdleme21ct  40323  cdleme21d  40324  cdleme21e  40325  cdleme22cN  40336  cdleme22f  40340  cdleme22f2  40341  cdleme23a  40343  cdleme23b  40344  cdleme23c  40345  cdleme25a  40347  cdleme25dN  40350  cdleme26fALTN  40356  cdleme26f  40357  cdleme26f2ALTN  40358  cdleme26f2  40359  cdlemefr29bpre0N  40400  cdlemefr29clN  40401  cdlemefr32fvaN  40403  cdlemefr32fva1  40404  cdleme41sn3a  40427  cdleme32le  40441  cdleme35a  40442  cdleme35fnpq  40443  cdleme35b  40444  cdleme35c  40445  cdleme35d  40446  cdleme35e  40447  cdleme35f  40448  cdleme36a  40454  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  trlord  40563  cdlemb3  40600  cdlemg7fvbwN  40601  cdlemg7aN  40619  cdlemg10a  40634  cdlemg10  40635  cdlemg12d  40640  cdlemg12e  40641  cdlemg12f  40642  cdlemg12g  40643  cdlemg12  40644  cdlemg13a  40645  cdlemg13  40646  cdlemg17b  40656  cdlemg17f  40660  cdlemg17g  40661  cdlemg17h  40662  cdlemg17pq  40666  cdlemg17  40671  cdlemg19a  40677  cdlemg19  40678  cdlemg21  40680  cdlemg27a  40686  cdlemg27b  40690  cdlemg31c  40693  cdlemg33b0  40695  cdlemg33a  40700  trlcone  40722  cdlemg44  40727  cdlemg48  40731  cdlemk37  40908  cdlemky  40920  cdlemk11ta  40923  cdleml4N  40973  dihord1  41212  dihord2pre2  41220  dihord4  41252  dihord5apre  41256  dihmeetlem1N  41284  dihglblem3N  41289  dihglbcpreN  41294  dihmeetlem3N  41299  dihmeetlem13N  41313  mapdpglem32  41699  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  mzpcong  42961  iscnrm3rlem8  48935