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  10339  axcontlem4  29575  eqlkr  40348  athgt  40705  llncvrlpln2  40806  4atlem11b  40857  2lnat  41033  cdlemblem  41042  pclfinN  41149  lhp2lt  41250  lhpmcvr5N  41276  lhpmcvr6N  41277  lhp2at0  41281  lhp2atnle  41282  lhp2at0nle  41284  4atexlemex6  41323  cdlemd2  41448  cdlemd7  41453  cdlemd8  41454  cdlemd9  41455  cdleme7aa  41491  cdleme7c  41494  cdleme7d  41495  cdleme7e  41496  cdleme7ga  41497  cdleme7  41498  cdleme11c  41510  cdleme11dN  41511  cdleme11e  41512  cdleme11  41519  cdleme14  41522  cdleme15a  41523  cdleme15b  41524  cdleme15d  41526  cdleme15  41527  cdleme16b  41528  cdleme16c  41529  cdleme16d  41530  cdleme18d  41544  cdleme19b  41553  cdleme19e  41556  cdleme20d  41561  cdleme20g  41564  cdleme20h  41565  cdleme20i  41566  cdleme20j  41567  cdleme20l2  41570  cdleme20l  41571  cdleme20m  41572  cdleme21c  41576  cdleme21ct  41578  cdleme21d  41579  cdleme21e  41580  cdleme22cN  41591  cdleme22f  41595  cdleme22f2  41596  cdleme23a  41598  cdleme23b  41599  cdleme23c  41600  cdleme25a  41602  cdleme25dN  41605  cdleme26fALTN  41611  cdleme26f  41612  cdleme26f2ALTN  41613  cdleme26f2  41614  cdlemefr29bpre0N  41655  cdlemefr29clN  41656  cdlemefr32fvaN  41658  cdlemefr32fva1  41659  cdleme41sn3a  41682  cdleme32le  41696  cdleme35a  41697  cdleme35fnpq  41698  cdleme35b  41699  cdleme35c  41700  cdleme35d  41701  cdleme35e  41702  cdleme35f  41703  cdleme36a  41709  cdleme37m  41711  cdleme39n  41715  cdleme43bN  41739  cdleme43dN  41741  cdleme17d2  41744  cdlemeg46c  41762  cdlemeg46nlpq  41766  cdlemeg46ngfr  41767  cdlemeg46req  41778  cdlemeg46gfv  41779  cdleme50trn1  41798  cdleme50trn2a  41799  cdlemf1  41810  trlord  41818  cdlemb3  41855  cdlemg7fvbwN  41856  cdlemg7aN  41874  cdlemg10a  41889  cdlemg10  41890  cdlemg12d  41895  cdlemg12e  41896  cdlemg12f  41897  cdlemg12g  41898  cdlemg12  41899  cdlemg13a  41900  cdlemg13  41901  cdlemg17b  41911  cdlemg17f  41915  cdlemg17g  41916  cdlemg17h  41917  cdlemg17pq  41921  cdlemg17  41926  cdlemg19a  41932  cdlemg19  41933  cdlemg21  41935  cdlemg27a  41941  cdlemg27b  41945  cdlemg31c  41948  cdlemg33b0  41950  cdlemg33a  41955  trlcone  41977  cdlemg44  41982  cdlemg48  41986  cdlemk37  42163  cdlemky  42175  cdlemk11ta  42178  cdleml4N  42228  dihord1  42467  dihord2pre2  42475  dihord4  42507  dihord5apre  42511  dihmeetlem1N  42539  dihglblem3N  42544  dihglbcpreN  42549  dihmeetlem3N  42554  dihmeetlem13N  42568  mapdpglem32  42954  baerlem3lem2  42959  baerlem5alem2  42960  baerlem5blem2  42961  mzpcong  44172  iscnrm3rlem8  50266