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  10144  axcontlem4  29040  eqlkr  39355  athgt  39712  llncvrlpln2  39813  4atlem11b  39864  2lnat  40040  cdlemblem  40049  pclfinN  40156  lhp2lt  40257  lhpmcvr5N  40283  lhpmcvr6N  40284  lhp2at0  40288  lhp2atnle  40289  lhp2at0nle  40291  4atexlemex6  40330  cdlemd2  40455  cdlemd7  40460  cdlemd8  40461  cdlemd9  40462  cdleme7aa  40498  cdleme7c  40501  cdleme7d  40502  cdleme7e  40503  cdleme7ga  40504  cdleme7  40505  cdleme11c  40517  cdleme11dN  40518  cdleme11e  40519  cdleme11  40526  cdleme14  40529  cdleme15a  40530  cdleme15b  40531  cdleme15d  40533  cdleme15  40534  cdleme16b  40535  cdleme16c  40536  cdleme16d  40537  cdleme18d  40551  cdleme19b  40560  cdleme19e  40563  cdleme20d  40568  cdleme20g  40571  cdleme20h  40572  cdleme20i  40573  cdleme20j  40574  cdleme20l2  40577  cdleme20l  40578  cdleme20m  40579  cdleme21c  40583  cdleme21ct  40585  cdleme21d  40586  cdleme21e  40587  cdleme22cN  40598  cdleme22f  40602  cdleme22f2  40603  cdleme23a  40605  cdleme23b  40606  cdleme23c  40607  cdleme25a  40609  cdleme25dN  40612  cdleme26fALTN  40618  cdleme26f  40619  cdleme26f2ALTN  40620  cdleme26f2  40621  cdlemefr29bpre0N  40662  cdlemefr29clN  40663  cdlemefr32fvaN  40665  cdlemefr32fva1  40666  cdleme41sn3a  40689  cdleme32le  40703  cdleme35a  40704  cdleme35fnpq  40705  cdleme35b  40706  cdleme35c  40707  cdleme35d  40708  cdleme35e  40709  cdleme35f  40710  cdleme36a  40716  cdleme37m  40718  cdleme39n  40722  cdleme43bN  40746  cdleme43dN  40748  cdleme17d2  40751  cdlemeg46c  40769  cdlemeg46nlpq  40773  cdlemeg46ngfr  40774  cdlemeg46req  40785  cdlemeg46gfv  40786  cdleme50trn1  40805  cdleme50trn2a  40806  cdlemf1  40817  trlord  40825  cdlemb3  40862  cdlemg7fvbwN  40863  cdlemg7aN  40881  cdlemg10a  40896  cdlemg10  40897  cdlemg12d  40902  cdlemg12e  40903  cdlemg12f  40904  cdlemg12g  40905  cdlemg12  40906  cdlemg13a  40907  cdlemg13  40908  cdlemg17b  40918  cdlemg17f  40922  cdlemg17g  40923  cdlemg17h  40924  cdlemg17pq  40928  cdlemg17  40933  cdlemg19a  40939  cdlemg19  40940  cdlemg21  40942  cdlemg27a  40948  cdlemg27b  40952  cdlemg31c  40955  cdlemg33b0  40957  cdlemg33a  40962  trlcone  40984  cdlemg44  40989  cdlemg48  40993  cdlemk37  41170  cdlemky  41182  cdlemk11ta  41185  cdleml4N  41235  dihord1  41474  dihord2pre2  41482  dihord4  41514  dihord5apre  41518  dihmeetlem1N  41546  dihglblem3N  41551  dihglbcpreN  41556  dihmeetlem3N  41561  dihmeetlem13N  41575  mapdpglem32  41961  baerlem3lem2  41966  baerlem5alem2  41967  baerlem5blem2  41968  mzpcong  43210  iscnrm3rlem8  49188