Theorem simp12l 1283

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

Assertion

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

Proof of Theorem simp12l

Step	Hyp	Ref	Expression
1		simp2l 1196	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜑)
2	1	3ad2ant1 1130	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  ackbij1lem16  9708  axcontlem4  26874  eqlkr  36710  athgt  37067  llncvrlpln2  37168  4atlem11b  37219  2lnat  37395  cdlemblem  37404  pclfinN  37511  lhp2lt  37612  lhpmcvr5N  37638  lhpmcvr6N  37639  lhp2at0  37643  lhp2atnle  37644  lhp2at0nle  37646  4atexlemex6  37685  cdlemd2  37810  cdlemd7  37815  cdlemd8  37816  cdlemd9  37817  cdleme7aa  37853  cdleme7c  37856  cdleme7d  37857  cdleme7e  37858  cdleme7ga  37859  cdleme7  37860  cdleme11c  37872  cdleme11dN  37873  cdleme11e  37874  cdleme11  37881  cdleme14  37884  cdleme15a  37885  cdleme15b  37886  cdleme15d  37888  cdleme15  37889  cdleme16b  37890  cdleme16c  37891  cdleme16d  37892  cdleme18d  37906  cdleme19b  37915  cdleme19e  37918  cdleme20d  37923  cdleme20g  37926  cdleme20h  37927  cdleme20i  37928  cdleme20j  37929  cdleme20l2  37932  cdleme20l  37933  cdleme20m  37934  cdleme21c  37938  cdleme21ct  37940  cdleme21d  37941  cdleme21e  37942  cdleme22cN  37953  cdleme22f  37957  cdleme22f2  37958  cdleme23a  37960  cdleme23b  37961  cdleme23c  37962  cdleme25a  37964  cdleme25dN  37967  cdleme26fALTN  37973  cdleme26f  37974  cdleme26f2ALTN  37975  cdleme26f2  37976  cdlemefr29bpre0N  38017  cdlemefr29clN  38018  cdlemefr32fvaN  38020  cdlemefr32fva1  38021  cdleme41sn3a  38044  cdleme32le  38058  cdleme35a  38059  cdleme35fnpq  38060  cdleme35b  38061  cdleme35c  38062  cdleme35d  38063  cdleme35e  38064  cdleme35f  38065  cdleme36a  38071  cdleme37m  38073  cdleme39n  38077  cdleme43bN  38101  cdleme43dN  38103  cdleme17d2  38106  cdlemeg46c  38124  cdlemeg46nlpq  38128  cdlemeg46ngfr  38129  cdlemeg46req  38140  cdlemeg46gfv  38141  cdleme50trn1  38160  cdleme50trn2a  38161  cdlemf1  38172  trlord  38180  cdlemb3  38217  cdlemg7fvbwN  38218  cdlemg7aN  38236  cdlemg10a  38251  cdlemg10  38252  cdlemg12d  38257  cdlemg12e  38258  cdlemg12f  38259  cdlemg12g  38260  cdlemg12  38261  cdlemg13a  38262  cdlemg13  38263  cdlemg17b  38273  cdlemg17f  38277  cdlemg17g  38278  cdlemg17h  38279  cdlemg17pq  38283  cdlemg17  38288  cdlemg19a  38294  cdlemg19  38295  cdlemg21  38297  cdlemg27a  38303  cdlemg27b  38307  cdlemg31c  38310  cdlemg33b0  38312  cdlemg33a  38317  trlcone  38339  cdlemg44  38344  cdlemg48  38348  cdlemk37  38525  cdlemky  38537  cdlemk11ta  38540  cdleml4N  38590  dihord1  38829  dihord2pre2  38837  dihord4  38869  dihord5apre  38873  dihmeetlem1N  38901  dihglblem3N  38906  dihglbcpreN  38911  dihmeetlem3N  38916  dihmeetlem13N  38930  mapdpglem32  39316  baerlem3lem2  39321  baerlem5alem2  39322  baerlem5blem2  39323  mzpcong  40331  iscnrm3rlem8  45692