Theorem simp12l 1287

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

Assertion

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

Proof of Theorem simp12l

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  ackbij1lem16  10230  axcontlem4  28225  eqlkr  37969  athgt  38327  llncvrlpln2  38428  4atlem11b  38479  2lnat  38655  cdlemblem  38664  pclfinN  38771  lhp2lt  38872  lhpmcvr5N  38898  lhpmcvr6N  38899  lhp2at0  38903  lhp2atnle  38904  lhp2at0nle  38906  4atexlemex6  38945  cdlemd2  39070  cdlemd7  39075  cdlemd8  39076  cdlemd9  39077  cdleme7aa  39113  cdleme7c  39116  cdleme7d  39117  cdleme7e  39118  cdleme7ga  39119  cdleme7  39120  cdleme11c  39132  cdleme11dN  39133  cdleme11e  39134  cdleme11  39141  cdleme14  39144  cdleme15a  39145  cdleme15b  39146  cdleme15d  39148  cdleme15  39149  cdleme16b  39150  cdleme16c  39151  cdleme16d  39152  cdleme18d  39166  cdleme19b  39175  cdleme19e  39178  cdleme20d  39183  cdleme20g  39186  cdleme20h  39187  cdleme20i  39188  cdleme20j  39189  cdleme20l2  39192  cdleme20l  39193  cdleme20m  39194  cdleme21c  39198  cdleme21ct  39200  cdleme21d  39201  cdleme21e  39202  cdleme22cN  39213  cdleme22f  39217  cdleme22f2  39218  cdleme23a  39220  cdleme23b  39221  cdleme23c  39222  cdleme25a  39224  cdleme25dN  39227  cdleme26fALTN  39233  cdleme26f  39234  cdleme26f2ALTN  39235  cdleme26f2  39236  cdlemefr29bpre0N  39277  cdlemefr29clN  39278  cdlemefr32fvaN  39280  cdlemefr32fva1  39281  cdleme41sn3a  39304  cdleme32le  39318  cdleme35a  39319  cdleme35fnpq  39320  cdleme35b  39321  cdleme35c  39322  cdleme35d  39323  cdleme35e  39324  cdleme35f  39325  cdleme36a  39331  cdleme37m  39333  cdleme39n  39337  cdleme43bN  39361  cdleme43dN  39363  cdleme17d2  39366  cdlemeg46c  39384  cdlemeg46nlpq  39388  cdlemeg46ngfr  39389  cdlemeg46req  39400  cdlemeg46gfv  39401  cdleme50trn1  39420  cdleme50trn2a  39421  cdlemf1  39432  trlord  39440  cdlemb3  39477  cdlemg7fvbwN  39478  cdlemg7aN  39496  cdlemg10a  39511  cdlemg10  39512  cdlemg12d  39517  cdlemg12e  39518  cdlemg12f  39519  cdlemg12g  39520  cdlemg12  39521  cdlemg13a  39522  cdlemg13  39523  cdlemg17b  39533  cdlemg17f  39537  cdlemg17g  39538  cdlemg17h  39539  cdlemg17pq  39543  cdlemg17  39548  cdlemg19a  39554  cdlemg19  39555  cdlemg21  39557  cdlemg27a  39563  cdlemg27b  39567  cdlemg31c  39570  cdlemg33b0  39572  cdlemg33a  39577  trlcone  39599  cdlemg44  39604  cdlemg48  39608  cdlemk37  39785  cdlemky  39797  cdlemk11ta  39800  cdleml4N  39850  dihord1  40089  dihord2pre2  40097  dihord4  40129  dihord5apre  40133  dihmeetlem1N  40161  dihglblem3N  40166  dihglbcpreN  40171  dihmeetlem3N  40176  dihmeetlem13N  40190  mapdpglem32  40576  baerlem3lem2  40581  baerlem5alem2  40582  baerlem5blem2  40583  mzpcong  41711  iscnrm3rlem8  47580