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 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ackbij1lem16  10303  axcontlem4  29000  eqlkr  39055  athgt  39413  llncvrlpln2  39514  4atlem11b  39565  2lnat  39741  cdlemblem  39750  pclfinN  39857  lhp2lt  39958  lhpmcvr5N  39984  lhpmcvr6N  39985  lhp2at0  39989  lhp2atnle  39990  lhp2at0nle  39992  4atexlemex6  40031  cdlemd2  40156  cdlemd7  40161  cdlemd8  40162  cdlemd9  40163  cdleme7aa  40199  cdleme7c  40202  cdleme7d  40203  cdleme7e  40204  cdleme7ga  40205  cdleme7  40206  cdleme11c  40218  cdleme11dN  40219  cdleme11e  40220  cdleme11  40227  cdleme14  40230  cdleme15a  40231  cdleme15b  40232  cdleme15d  40234  cdleme15  40235  cdleme16b  40236  cdleme16c  40237  cdleme16d  40238  cdleme18d  40252  cdleme19b  40261  cdleme19e  40264  cdleme20d  40269  cdleme20g  40272  cdleme20h  40273  cdleme20i  40274  cdleme20j  40275  cdleme20l2  40278  cdleme20l  40279  cdleme20m  40280  cdleme21c  40284  cdleme21ct  40286  cdleme21d  40287  cdleme21e  40288  cdleme22cN  40299  cdleme22f  40303  cdleme22f2  40304  cdleme23a  40306  cdleme23b  40307  cdleme23c  40308  cdleme25a  40310  cdleme25dN  40313  cdleme26fALTN  40319  cdleme26f  40320  cdleme26f2ALTN  40321  cdleme26f2  40322  cdlemefr29bpre0N  40363  cdlemefr29clN  40364  cdlemefr32fvaN  40366  cdlemefr32fva1  40367  cdleme41sn3a  40390  cdleme32le  40404  cdleme35a  40405  cdleme35fnpq  40406  cdleme35b  40407  cdleme35c  40408  cdleme35d  40409  cdleme35e  40410  cdleme35f  40411  cdleme36a  40417  cdleme37m  40419  cdleme39n  40423  cdleme43bN  40447  cdleme43dN  40449  cdleme17d2  40452  cdlemeg46c  40470  cdlemeg46nlpq  40474  cdlemeg46ngfr  40475  cdlemeg46req  40486  cdlemeg46gfv  40487  cdleme50trn1  40506  cdleme50trn2a  40507  cdlemf1  40518  trlord  40526  cdlemb3  40563  cdlemg7fvbwN  40564  cdlemg7aN  40582  cdlemg10a  40597  cdlemg10  40598  cdlemg12d  40603  cdlemg12e  40604  cdlemg12f  40605  cdlemg12g  40606  cdlemg12  40607  cdlemg13a  40608  cdlemg13  40609  cdlemg17b  40619  cdlemg17f  40623  cdlemg17g  40624  cdlemg17h  40625  cdlemg17pq  40629  cdlemg17  40634  cdlemg19a  40640  cdlemg19  40641  cdlemg21  40643  cdlemg27a  40649  cdlemg27b  40653  cdlemg31c  40656  cdlemg33b0  40658  cdlemg33a  40663  trlcone  40685  cdlemg44  40690  cdlemg48  40694  cdlemk37  40871  cdlemky  40883  cdlemk11ta  40886  cdleml4N  40936  dihord1  41175  dihord2pre2  41183  dihord4  41215  dihord5apre  41219  dihmeetlem1N  41247  dihglblem3N  41252  dihglbcpreN  41257  dihmeetlem3N  41262  dihmeetlem13N  41276  mapdpglem32  41662  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  mzpcong  42929  iscnrm3rlem8  48627