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  10246  axcontlem4  28892  eqlkr  39063  athgt  39421  llncvrlpln2  39522  4atlem11b  39573  2lnat  39749  cdlemblem  39758  pclfinN  39865  lhp2lt  39966  lhpmcvr5N  39992  lhpmcvr6N  39993  lhp2at0  39997  lhp2atnle  39998  lhp2at0nle  40000  4atexlemex6  40039  cdlemd2  40164  cdlemd7  40169  cdlemd8  40170  cdlemd9  40171  cdleme7aa  40207  cdleme7c  40210  cdleme7d  40211  cdleme7e  40212  cdleme7ga  40213  cdleme7  40214  cdleme11c  40226  cdleme11dN  40227  cdleme11e  40228  cdleme11  40235  cdleme14  40238  cdleme15a  40239  cdleme15b  40240  cdleme15d  40242  cdleme15  40243  cdleme16b  40244  cdleme16c  40245  cdleme16d  40246  cdleme18d  40260  cdleme19b  40269  cdleme19e  40272  cdleme20d  40277  cdleme20g  40280  cdleme20h  40281  cdleme20i  40282  cdleme20j  40283  cdleme20l2  40286  cdleme20l  40287  cdleme20m  40288  cdleme21c  40292  cdleme21ct  40294  cdleme21d  40295  cdleme21e  40296  cdleme22cN  40307  cdleme22f  40311  cdleme22f2  40312  cdleme23a  40314  cdleme23b  40315  cdleme23c  40316  cdleme25a  40318  cdleme25dN  40321  cdleme26fALTN  40327  cdleme26f  40328  cdleme26f2ALTN  40329  cdleme26f2  40330  cdlemefr29bpre0N  40371  cdlemefr29clN  40372  cdlemefr32fvaN  40374  cdlemefr32fva1  40375  cdleme41sn3a  40398  cdleme32le  40412  cdleme35a  40413  cdleme35fnpq  40414  cdleme35b  40415  cdleme35c  40416  cdleme35d  40417  cdleme35e  40418  cdleme35f  40419  cdleme36a  40425  cdleme37m  40427  cdleme39n  40431  cdleme43bN  40455  cdleme43dN  40457  cdleme17d2  40460  cdlemeg46c  40478  cdlemeg46nlpq  40482  cdlemeg46ngfr  40483  cdlemeg46req  40494  cdlemeg46gfv  40495  cdleme50trn1  40514  cdleme50trn2a  40515  cdlemf1  40526  trlord  40534  cdlemb3  40571  cdlemg7fvbwN  40572  cdlemg7aN  40590  cdlemg10a  40605  cdlemg10  40606  cdlemg12d  40611  cdlemg12e  40612  cdlemg12f  40613  cdlemg12g  40614  cdlemg12  40615  cdlemg13a  40616  cdlemg13  40617  cdlemg17b  40627  cdlemg17f  40631  cdlemg17g  40632  cdlemg17h  40633  cdlemg17pq  40637  cdlemg17  40642  cdlemg19a  40648  cdlemg19  40649  cdlemg21  40651  cdlemg27a  40657  cdlemg27b  40661  cdlemg31c  40664  cdlemg33b0  40666  cdlemg33a  40671  trlcone  40693  cdlemg44  40698  cdlemg48  40702  cdlemk37  40879  cdlemky  40891  cdlemk11ta  40894  cdleml4N  40944  dihord1  41183  dihord2pre2  41191  dihord4  41223  dihord5apre  41227  dihmeetlem1N  41255  dihglblem3N  41260  dihglbcpreN  41265  dihmeetlem3N  41270  dihmeetlem13N  41284  mapdpglem32  41670  baerlem3lem2  41675  baerlem5alem2  41676  baerlem5blem2  41677  mzpcong  42943  iscnrm3rlem8  48869