Theorem simp12l 1305

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

Assertion

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

Proof of Theorem simp12l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ackbij1lem16  10236  axcontlem4  29354  eqlkr  39914  athgt  40271  llncvrlpln2  40372  4atlem11b  40423  2lnat  40599  cdlemblem  40608  pclfinN  40715  lhp2lt  40816  lhpmcvr5N  40842  lhpmcvr6N  40843  lhp2at0  40847  lhp2atnle  40848  lhp2at0nle  40850  4atexlemex6  40889  cdlemd2  41014  cdlemd7  41019  cdlemd8  41020  cdlemd9  41021  cdleme7aa  41057  cdleme7c  41060  cdleme7d  41061  cdleme7e  41062  cdleme7ga  41063  cdleme7  41064  cdleme11c  41076  cdleme11dN  41077  cdleme11e  41078  cdleme11  41085  cdleme14  41088  cdleme15a  41089  cdleme15b  41090  cdleme15d  41092  cdleme15  41093  cdleme16b  41094  cdleme16c  41095  cdleme16d  41096  cdleme18d  41110  cdleme19b  41119  cdleme19e  41122  cdleme20d  41127  cdleme20g  41130  cdleme20h  41131  cdleme20i  41132  cdleme20j  41133  cdleme20l2  41136  cdleme20l  41137  cdleme20m  41138  cdleme21c  41142  cdleme21ct  41144  cdleme21d  41145  cdleme21e  41146  cdleme22cN  41157  cdleme22f  41161  cdleme22f2  41162  cdleme23a  41164  cdleme23b  41165  cdleme23c  41166  cdleme25a  41168  cdleme25dN  41171  cdleme26fALTN  41177  cdleme26f  41178  cdleme26f2ALTN  41179  cdleme26f2  41180  cdlemefr29bpre0N  41221  cdlemefr29clN  41222  cdlemefr32fvaN  41224  cdlemefr32fva1  41225  cdleme41sn3a  41248  cdleme32le  41262  cdleme35a  41263  cdleme35fnpq  41264  cdleme35b  41265  cdleme35c  41266  cdleme35d  41267  cdleme35e  41268  cdleme35f  41269  cdleme36a  41275  cdleme37m  41277  cdleme39n  41281  cdleme43bN  41305  cdleme43dN  41307  cdleme17d2  41310  cdlemeg46c  41328  cdlemeg46nlpq  41332  cdlemeg46ngfr  41333  cdlemeg46req  41344  cdlemeg46gfv  41345  cdleme50trn1  41364  cdleme50trn2a  41365  cdlemf1  41376  trlord  41384  cdlemb3  41421  cdlemg7fvbwN  41422  cdlemg7aN  41440  cdlemg10a  41455  cdlemg10  41456  cdlemg12d  41461  cdlemg12e  41462  cdlemg12f  41463  cdlemg12g  41464  cdlemg12  41465  cdlemg13a  41466  cdlemg13  41467  cdlemg17b  41477  cdlemg17f  41481  cdlemg17g  41482  cdlemg17h  41483  cdlemg17pq  41487  cdlemg17  41492  cdlemg19a  41498  cdlemg19  41499  cdlemg21  41501  cdlemg27a  41507  cdlemg27b  41511  cdlemg31c  41514  cdlemg33b0  41516  cdlemg33a  41521  trlcone  41543  cdlemg44  41548  cdlemg48  41552  cdlemk37  41729  cdlemky  41741  cdlemk11ta  41744  cdleml4N  41794  dihord1  42033  dihord2pre2  42041  dihord4  42073  dihord5apre  42077  dihmeetlem1N  42105  dihglblem3N  42110  dihglbcpreN  42115  dihmeetlem3N  42120  dihmeetlem13N  42134  mapdpglem32  42520  baerlem3lem2  42525  baerlem5alem2  42526  baerlem5blem2  42527  mzpcong  43740  iscnrm3rlem8  49766