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  10122  axcontlem4  28943  eqlkr  39137  athgt  39494  llncvrlpln2  39595  4atlem11b  39646  2lnat  39822  cdlemblem  39831  pclfinN  39938  lhp2lt  40039  lhpmcvr5N  40065  lhpmcvr6N  40066  lhp2at0  40070  lhp2atnle  40071  lhp2at0nle  40073  4atexlemex6  40112  cdlemd2  40237  cdlemd7  40242  cdlemd8  40243  cdlemd9  40244  cdleme7aa  40280  cdleme7c  40283  cdleme7d  40284  cdleme7e  40285  cdleme7ga  40286  cdleme7  40287  cdleme11c  40299  cdleme11dN  40300  cdleme11e  40301  cdleme11  40308  cdleme14  40311  cdleme15a  40312  cdleme15b  40313  cdleme15d  40315  cdleme15  40316  cdleme16b  40317  cdleme16c  40318  cdleme16d  40319  cdleme18d  40333  cdleme19b  40342  cdleme19e  40345  cdleme20d  40350  cdleme20g  40353  cdleme20h  40354  cdleme20i  40355  cdleme20j  40356  cdleme20l2  40359  cdleme20l  40360  cdleme20m  40361  cdleme21c  40365  cdleme21ct  40367  cdleme21d  40368  cdleme21e  40369  cdleme22cN  40380  cdleme22f  40384  cdleme22f2  40385  cdleme23a  40387  cdleme23b  40388  cdleme23c  40389  cdleme25a  40391  cdleme25dN  40394  cdleme26fALTN  40400  cdleme26f  40401  cdleme26f2ALTN  40402  cdleme26f2  40403  cdlemefr29bpre0N  40444  cdlemefr29clN  40445  cdlemefr32fvaN  40447  cdlemefr32fva1  40448  cdleme41sn3a  40471  cdleme32le  40485  cdleme35a  40486  cdleme35fnpq  40487  cdleme35b  40488  cdleme35c  40489  cdleme35d  40490  cdleme35e  40491  cdleme35f  40492  cdleme36a  40498  cdleme37m  40500  cdleme39n  40504  cdleme43bN  40528  cdleme43dN  40530  cdleme17d2  40533  cdlemeg46c  40551  cdlemeg46nlpq  40555  cdlemeg46ngfr  40556  cdlemeg46req  40567  cdlemeg46gfv  40568  cdleme50trn1  40587  cdleme50trn2a  40588  cdlemf1  40599  trlord  40607  cdlemb3  40644  cdlemg7fvbwN  40645  cdlemg7aN  40663  cdlemg10a  40678  cdlemg10  40679  cdlemg12d  40684  cdlemg12e  40685  cdlemg12f  40686  cdlemg12g  40687  cdlemg12  40688  cdlemg13a  40689  cdlemg13  40690  cdlemg17b  40700  cdlemg17f  40704  cdlemg17g  40705  cdlemg17h  40706  cdlemg17pq  40710  cdlemg17  40715  cdlemg19a  40721  cdlemg19  40722  cdlemg21  40724  cdlemg27a  40730  cdlemg27b  40734  cdlemg31c  40737  cdlemg33b0  40739  cdlemg33a  40744  trlcone  40766  cdlemg44  40771  cdlemg48  40775  cdlemk37  40952  cdlemky  40964  cdlemk11ta  40967  cdleml4N  41017  dihord1  41256  dihord2pre2  41264  dihord4  41296  dihord5apre  41300  dihmeetlem1N  41328  dihglblem3N  41333  dihglbcpreN  41338  dihmeetlem3N  41343  dihmeetlem13N  41357  mapdpglem32  41743  baerlem3lem2  41748  baerlem5alem2  41749  baerlem5blem2  41750  mzpcong  43004  iscnrm3rlem8  48977