Theorem simp12l 1283

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

Assertion

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

Proof of Theorem simp12l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  ackbij1lem16  9646  axcontlem4  26761  eqlkr  36395  athgt  36752  llncvrlpln2  36853  4atlem11b  36904  2lnat  37080  cdlemblem  37089  pclfinN  37196  lhp2lt  37297  lhpmcvr5N  37323  lhpmcvr6N  37324  lhp2at0  37328  lhp2atnle  37329  lhp2at0nle  37331  4atexlemex6  37370  cdlemd2  37495  cdlemd7  37500  cdlemd8  37501  cdlemd9  37502  cdleme7aa  37538  cdleme7c  37541  cdleme7d  37542  cdleme7e  37543  cdleme7ga  37544  cdleme7  37545  cdleme11c  37557  cdleme11dN  37558  cdleme11e  37559  cdleme11  37566  cdleme14  37569  cdleme15a  37570  cdleme15b  37571  cdleme15d  37573  cdleme15  37574  cdleme16b  37575  cdleme16c  37576  cdleme16d  37577  cdleme18d  37591  cdleme19b  37600  cdleme19e  37603  cdleme20d  37608  cdleme20g  37611  cdleme20h  37612  cdleme20i  37613  cdleme20j  37614  cdleme20l2  37617  cdleme20l  37618  cdleme20m  37619  cdleme21c  37623  cdleme21ct  37625  cdleme21d  37626  cdleme21e  37627  cdleme22cN  37638  cdleme22f  37642  cdleme22f2  37643  cdleme23a  37645  cdleme23b  37646  cdleme23c  37647  cdleme25a  37649  cdleme25dN  37652  cdleme26fALTN  37658  cdleme26f  37659  cdleme26f2ALTN  37660  cdleme26f2  37661  cdlemefr29bpre0N  37702  cdlemefr29clN  37703  cdlemefr32fvaN  37705  cdlemefr32fva1  37706  cdleme41sn3a  37729  cdleme32le  37743  cdleme35a  37744  cdleme35fnpq  37745  cdleme35b  37746  cdleme35c  37747  cdleme35d  37748  cdleme35e  37749  cdleme35f  37750  cdleme36a  37756  cdleme37m  37758  cdleme39n  37762  cdleme43bN  37786  cdleme43dN  37788  cdleme17d2  37791  cdlemeg46c  37809  cdlemeg46nlpq  37813  cdlemeg46ngfr  37814  cdlemeg46req  37825  cdlemeg46gfv  37826  cdleme50trn1  37845  cdleme50trn2a  37846  cdlemf1  37857  trlord  37865  cdlemb3  37902  cdlemg7fvbwN  37903  cdlemg7aN  37921  cdlemg10a  37936  cdlemg10  37937  cdlemg12d  37942  cdlemg12e  37943  cdlemg12f  37944  cdlemg12g  37945  cdlemg12  37946  cdlemg13a  37947  cdlemg13  37948  cdlemg17b  37958  cdlemg17f  37962  cdlemg17g  37963  cdlemg17h  37964  cdlemg17pq  37968  cdlemg17  37973  cdlemg19a  37979  cdlemg19  37980  cdlemg21  37982  cdlemg27a  37988  cdlemg27b  37992  cdlemg31c  37995  cdlemg33b0  37997  cdlemg33a  38002  trlcone  38024  cdlemg44  38029  cdlemg48  38033  cdlemk37  38210  cdlemky  38222  cdlemk11ta  38225  cdleml4N  38275  dihord1  38514  dihord2pre2  38522  dihord4  38554  dihord5apre  38558  dihmeetlem1N  38586  dihglblem3N  38591  dihglbcpreN  38596  dihmeetlem3N  38601  dihmeetlem13N  38615  mapdpglem32  39001  baerlem3lem2  39006  baerlem5alem2  39007  baerlem5blem2  39008  mzpcong  39913