Theorem simp12l 1293

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

Assertion

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

Proof of Theorem simp12l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ackbij1lem16  10154  axcontlem4  29061  eqlkr  39598  athgt  39955  llncvrlpln2  40056  4atlem11b  40107  2lnat  40283  cdlemblem  40292  pclfinN  40399  lhp2lt  40500  lhpmcvr5N  40526  lhpmcvr6N  40527  lhp2at0  40531  lhp2atnle  40532  lhp2at0nle  40534  4atexlemex6  40573  cdlemd2  40698  cdlemd7  40703  cdlemd8  40704  cdlemd9  40705  cdleme7aa  40741  cdleme7c  40744  cdleme7d  40745  cdleme7e  40746  cdleme7ga  40747  cdleme7  40748  cdleme11c  40760  cdleme11dN  40761  cdleme11e  40762  cdleme11  40769  cdleme14  40772  cdleme15a  40773  cdleme15b  40774  cdleme15d  40776  cdleme15  40777  cdleme16b  40778  cdleme16c  40779  cdleme16d  40780  cdleme18d  40794  cdleme19b  40803  cdleme19e  40806  cdleme20d  40811  cdleme20g  40814  cdleme20h  40815  cdleme20i  40816  cdleme20j  40817  cdleme20l2  40820  cdleme20l  40821  cdleme20m  40822  cdleme21c  40826  cdleme21ct  40828  cdleme21d  40829  cdleme21e  40830  cdleme22cN  40841  cdleme22f  40845  cdleme22f2  40846  cdleme23a  40848  cdleme23b  40849  cdleme23c  40850  cdleme25a  40852  cdleme25dN  40855  cdleme26fALTN  40861  cdleme26f  40862  cdleme26f2ALTN  40863  cdleme26f2  40864  cdlemefr29bpre0N  40905  cdlemefr29clN  40906  cdlemefr32fvaN  40908  cdlemefr32fva1  40909  cdleme41sn3a  40932  cdleme32le  40946  cdleme35a  40947  cdleme35fnpq  40948  cdleme35b  40949  cdleme35c  40950  cdleme35d  40951  cdleme35e  40952  cdleme35f  40953  cdleme36a  40959  cdleme37m  40961  cdleme39n  40965  cdleme43bN  40989  cdleme43dN  40991  cdleme17d2  40994  cdlemeg46c  41012  cdlemeg46nlpq  41016  cdlemeg46ngfr  41017  cdlemeg46req  41028  cdlemeg46gfv  41029  cdleme50trn1  41048  cdleme50trn2a  41049  cdlemf1  41060  trlord  41068  cdlemb3  41105  cdlemg7fvbwN  41106  cdlemg7aN  41124  cdlemg10a  41139  cdlemg10  41140  cdlemg12d  41145  cdlemg12e  41146  cdlemg12f  41147  cdlemg12g  41148  cdlemg12  41149  cdlemg13a  41150  cdlemg13  41151  cdlemg17b  41161  cdlemg17f  41165  cdlemg17g  41166  cdlemg17h  41167  cdlemg17pq  41171  cdlemg17  41176  cdlemg19a  41182  cdlemg19  41183  cdlemg21  41185  cdlemg27a  41191  cdlemg27b  41195  cdlemg31c  41198  cdlemg33b0  41200  cdlemg33a  41205  trlcone  41227  cdlemg44  41232  cdlemg48  41236  cdlemk37  41413  cdlemky  41425  cdlemk11ta  41428  cdleml4N  41478  dihord1  41717  dihord2pre2  41725  dihord4  41757  dihord5apre  41761  dihmeetlem1N  41789  dihglblem3N  41794  dihglbcpreN  41799  dihmeetlem3N  41804  dihmeetlem13N  41818  mapdpglem32  42204  baerlem3lem2  42209  baerlem5alem2  42210  baerlem5blem2  42211  mzpcong  43424  iscnrm3rlem8  49444