Theorem simp12l 1285

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

Assertion

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

Proof of Theorem simp12l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ackbij1lem16  10000  axcontlem4  27344  eqlkr  37120  athgt  37477  llncvrlpln2  37578  4atlem11b  37629  2lnat  37805  cdlemblem  37814  pclfinN  37921  lhp2lt  38022  lhpmcvr5N  38048  lhpmcvr6N  38049  lhp2at0  38053  lhp2atnle  38054  lhp2at0nle  38056  4atexlemex6  38095  cdlemd2  38220  cdlemd7  38225  cdlemd8  38226  cdlemd9  38227  cdleme7aa  38263  cdleme7c  38266  cdleme7d  38267  cdleme7e  38268  cdleme7ga  38269  cdleme7  38270  cdleme11c  38282  cdleme11dN  38283  cdleme11e  38284  cdleme11  38291  cdleme14  38294  cdleme15a  38295  cdleme15b  38296  cdleme15d  38298  cdleme15  38299  cdleme16b  38300  cdleme16c  38301  cdleme16d  38302  cdleme18d  38316  cdleme19b  38325  cdleme19e  38328  cdleme20d  38333  cdleme20g  38336  cdleme20h  38337  cdleme20i  38338  cdleme20j  38339  cdleme20l2  38342  cdleme20l  38343  cdleme20m  38344  cdleme21c  38348  cdleme21ct  38350  cdleme21d  38351  cdleme21e  38352  cdleme22cN  38363  cdleme22f  38367  cdleme22f2  38368  cdleme23a  38370  cdleme23b  38371  cdleme23c  38372  cdleme25a  38374  cdleme25dN  38377  cdleme26fALTN  38383  cdleme26f  38384  cdleme26f2ALTN  38385  cdleme26f2  38386  cdlemefr29bpre0N  38427  cdlemefr29clN  38428  cdlemefr32fvaN  38430  cdlemefr32fva1  38431  cdleme41sn3a  38454  cdleme32le  38468  cdleme35a  38469  cdleme35fnpq  38470  cdleme35b  38471  cdleme35c  38472  cdleme35d  38473  cdleme35e  38474  cdleme35f  38475  cdleme36a  38481  cdleme37m  38483  cdleme39n  38487  cdleme43bN  38511  cdleme43dN  38513  cdleme17d2  38516  cdlemeg46c  38534  cdlemeg46nlpq  38538  cdlemeg46ngfr  38539  cdlemeg46req  38550  cdlemeg46gfv  38551  cdleme50trn1  38570  cdleme50trn2a  38571  cdlemf1  38582  trlord  38590  cdlemb3  38627  cdlemg7fvbwN  38628  cdlemg7aN  38646  cdlemg10a  38661  cdlemg10  38662  cdlemg12d  38667  cdlemg12e  38668  cdlemg12f  38669  cdlemg12g  38670  cdlemg12  38671  cdlemg13a  38672  cdlemg13  38673  cdlemg17b  38683  cdlemg17f  38687  cdlemg17g  38688  cdlemg17h  38689  cdlemg17pq  38693  cdlemg17  38698  cdlemg19a  38704  cdlemg19  38705  cdlemg21  38707  cdlemg27a  38713  cdlemg27b  38717  cdlemg31c  38720  cdlemg33b0  38722  cdlemg33a  38727  trlcone  38749  cdlemg44  38754  cdlemg48  38758  cdlemk37  38935  cdlemky  38947  cdlemk11ta  38950  cdleml4N  39000  dihord1  39239  dihord2pre2  39247  dihord4  39279  dihord5apre  39283  dihmeetlem1N  39311  dihglblem3N  39316  dihglbcpreN  39321  dihmeetlem3N  39326  dihmeetlem13N  39340  mapdpglem32  39726  baerlem3lem2  39731  baerlem5alem2  39732  baerlem5blem2  39733  mzpcong  40801  iscnrm3rlem8  46252