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 1133	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)

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

This theorem is referenced by:  ackbij1lem16  10147  axcontlem4  28930  eqlkr  39077  athgt  39435  llncvrlpln2  39536  4atlem11b  39587  2lnat  39763  cdlemblem  39772  pclfinN  39879  lhp2lt  39980  lhpmcvr5N  40006  lhpmcvr6N  40007  lhp2at0  40011  lhp2atnle  40012  lhp2at0nle  40014  4atexlemex6  40053  cdlemd2  40178  cdlemd7  40183  cdlemd8  40184  cdlemd9  40185  cdleme7aa  40221  cdleme7c  40224  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme7  40228  cdleme11c  40240  cdleme11dN  40241  cdleme11e  40242  cdleme11  40249  cdleme14  40252  cdleme15a  40253  cdleme15b  40254  cdleme15d  40256  cdleme15  40257  cdleme16b  40258  cdleme16c  40259  cdleme16d  40260  cdleme18d  40274  cdleme19b  40283  cdleme19e  40286  cdleme20d  40291  cdleme20g  40294  cdleme20h  40295  cdleme20i  40296  cdleme20j  40297  cdleme20l2  40300  cdleme20l  40301  cdleme20m  40302  cdleme21c  40306  cdleme21ct  40308  cdleme21d  40309  cdleme21e  40310  cdleme22cN  40321  cdleme22f  40325  cdleme22f2  40326  cdleme23a  40328  cdleme23b  40329  cdleme23c  40330  cdleme25a  40332  cdleme25dN  40335  cdleme26fALTN  40341  cdleme26f  40342  cdleme26f2ALTN  40343  cdleme26f2  40344  cdlemefr29bpre0N  40385  cdlemefr29clN  40386  cdlemefr32fvaN  40388  cdlemefr32fva1  40389  cdleme41sn3a  40412  cdleme32le  40426  cdleme35a  40427  cdleme35fnpq  40428  cdleme35b  40429  cdleme35c  40430  cdleme35d  40431  cdleme35e  40432  cdleme35f  40433  cdleme36a  40439  cdleme37m  40441  cdleme39n  40445  cdleme43bN  40469  cdleme43dN  40471  cdleme17d2  40474  cdlemeg46c  40492  cdlemeg46nlpq  40496  cdlemeg46ngfr  40497  cdlemeg46req  40508  cdlemeg46gfv  40509  cdleme50trn1  40528  cdleme50trn2a  40529  cdlemf1  40540  trlord  40548  cdlemb3  40585  cdlemg7fvbwN  40586  cdlemg7aN  40604  cdlemg10a  40619  cdlemg10  40620  cdlemg12d  40625  cdlemg12e  40626  cdlemg12f  40627  cdlemg12g  40628  cdlemg12  40629  cdlemg13a  40630  cdlemg13  40631  cdlemg17b  40641  cdlemg17f  40645  cdlemg17g  40646  cdlemg17h  40647  cdlemg17pq  40651  cdlemg17  40656  cdlemg19a  40662  cdlemg19  40663  cdlemg21  40665  cdlemg27a  40671  cdlemg27b  40675  cdlemg31c  40678  cdlemg33b0  40680  cdlemg33a  40685  trlcone  40707  cdlemg44  40712  cdlemg48  40716  cdlemk37  40893  cdlemky  40905  cdlemk11ta  40908  cdleml4N  40958  dihord1  41197  dihord2pre2  41205  dihord4  41237  dihord5apre  41241  dihmeetlem1N  41269  dihglblem3N  41274  dihglbcpreN  41279  dihmeetlem3N  41284  dihmeetlem13N  41298  mapdpglem32  41684  baerlem3lem2  41689  baerlem5alem2  41690  baerlem5blem2  41691  mzpcong  42945  iscnrm3rlem8  48932