Theorem simp12l 1286

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

Assertion

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

Proof of Theorem simp12l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 1089

This theorem is referenced by:  ackbij1lem16  10229  axcontlem4  28222  eqlkr  37964  athgt  38322  llncvrlpln2  38423  4atlem11b  38474  2lnat  38650  cdlemblem  38659  pclfinN  38766  lhp2lt  38867  lhpmcvr5N  38893  lhpmcvr6N  38894  lhp2at0  38898  lhp2atnle  38899  lhp2at0nle  38901  4atexlemex6  38940  cdlemd2  39065  cdlemd7  39070  cdlemd8  39071  cdlemd9  39072  cdleme7aa  39108  cdleme7c  39111  cdleme7d  39112  cdleme7e  39113  cdleme7ga  39114  cdleme7  39115  cdleme11c  39127  cdleme11dN  39128  cdleme11e  39129  cdleme11  39136  cdleme14  39139  cdleme15a  39140  cdleme15b  39141  cdleme15d  39143  cdleme15  39144  cdleme16b  39145  cdleme16c  39146  cdleme16d  39147  cdleme18d  39161  cdleme19b  39170  cdleme19e  39173  cdleme20d  39178  cdleme20g  39181  cdleme20h  39182  cdleme20i  39183  cdleme20j  39184  cdleme20l2  39187  cdleme20l  39188  cdleme20m  39189  cdleme21c  39193  cdleme21ct  39195  cdleme21d  39196  cdleme21e  39197  cdleme22cN  39208  cdleme22f  39212  cdleme22f2  39213  cdleme23a  39215  cdleme23b  39216  cdleme23c  39217  cdleme25a  39219  cdleme25dN  39222  cdleme26fALTN  39228  cdleme26f  39229  cdleme26f2ALTN  39230  cdleme26f2  39231  cdlemefr29bpre0N  39272  cdlemefr29clN  39273  cdlemefr32fvaN  39275  cdlemefr32fva1  39276  cdleme41sn3a  39299  cdleme32le  39313  cdleme35a  39314  cdleme35fnpq  39315  cdleme35b  39316  cdleme35c  39317  cdleme35d  39318  cdleme35e  39319  cdleme35f  39320  cdleme36a  39326  cdleme37m  39328  cdleme39n  39332  cdleme43bN  39356  cdleme43dN  39358  cdleme17d2  39361  cdlemeg46c  39379  cdlemeg46nlpq  39383  cdlemeg46ngfr  39384  cdlemeg46req  39395  cdlemeg46gfv  39396  cdleme50trn1  39415  cdleme50trn2a  39416  cdlemf1  39427  trlord  39435  cdlemb3  39472  cdlemg7fvbwN  39473  cdlemg7aN  39491  cdlemg10a  39506  cdlemg10  39507  cdlemg12d  39512  cdlemg12e  39513  cdlemg12f  39514  cdlemg12g  39515  cdlemg12  39516  cdlemg13a  39517  cdlemg13  39518  cdlemg17b  39528  cdlemg17f  39532  cdlemg17g  39533  cdlemg17h  39534  cdlemg17pq  39538  cdlemg17  39543  cdlemg19a  39549  cdlemg19  39550  cdlemg21  39552  cdlemg27a  39558  cdlemg27b  39562  cdlemg31c  39565  cdlemg33b0  39567  cdlemg33a  39572  trlcone  39594  cdlemg44  39599  cdlemg48  39603  cdlemk37  39780  cdlemky  39792  cdlemk11ta  39795  cdleml4N  39845  dihord1  40084  dihord2pre2  40092  dihord4  40124  dihord5apre  40128  dihmeetlem1N  40156  dihglblem3N  40161  dihglbcpreN  40166  dihmeetlem3N  40171  dihmeetlem13N  40185  mapdpglem32  40571  baerlem3lem2  40576  baerlem5alem2  40577  baerlem5blem2  40578  mzpcong  41701  iscnrm3rlem8  47570