Theorem simp12l 1285

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

Assertion

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

Proof of Theorem simp12l

Step	Hyp	Ref	Expression
1		simp2l 1198	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜑)
2	1	3ad2ant1 1132	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  10271  axcontlem4  28996  eqlkr  39080  athgt  39438  llncvrlpln2  39539  4atlem11b  39590  2lnat  39766  cdlemblem  39775  pclfinN  39882  lhp2lt  39983  lhpmcvr5N  40009  lhpmcvr6N  40010  lhp2at0  40014  lhp2atnle  40015  lhp2at0nle  40017  4atexlemex6  40056  cdlemd2  40181  cdlemd7  40186  cdlemd8  40187  cdlemd9  40188  cdleme7aa  40224  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme7  40231  cdleme11c  40243  cdleme11dN  40244  cdleme11e  40245  cdleme11  40252  cdleme14  40255  cdleme15a  40256  cdleme15b  40257  cdleme15d  40259  cdleme15  40260  cdleme16b  40261  cdleme16c  40262  cdleme16d  40263  cdleme18d  40277  cdleme19b  40286  cdleme19e  40289  cdleme20d  40294  cdleme20g  40297  cdleme20h  40298  cdleme20i  40299  cdleme20j  40300  cdleme20l2  40303  cdleme20l  40304  cdleme20m  40305  cdleme21c  40309  cdleme21ct  40311  cdleme21d  40312  cdleme21e  40313  cdleme22cN  40324  cdleme22f  40328  cdleme22f2  40329  cdleme23a  40331  cdleme23b  40332  cdleme23c  40333  cdleme25a  40335  cdleme25dN  40338  cdleme26fALTN  40344  cdleme26f  40345  cdleme26f2ALTN  40346  cdleme26f2  40347  cdlemefr29bpre0N  40388  cdlemefr29clN  40389  cdlemefr32fvaN  40391  cdlemefr32fva1  40392  cdleme41sn3a  40415  cdleme32le  40429  cdleme35a  40430  cdleme35fnpq  40431  cdleme35b  40432  cdleme35c  40433  cdleme35d  40434  cdleme35e  40435  cdleme35f  40436  cdleme36a  40442  cdleme37m  40444  cdleme39n  40448  cdleme43bN  40472  cdleme43dN  40474  cdleme17d2  40477  cdlemeg46c  40495  cdlemeg46nlpq  40499  cdlemeg46ngfr  40500  cdlemeg46req  40511  cdlemeg46gfv  40512  cdleme50trn1  40531  cdleme50trn2a  40532  cdlemf1  40543  trlord  40551  cdlemb3  40588  cdlemg7fvbwN  40589  cdlemg7aN  40607  cdlemg10a  40622  cdlemg10  40623  cdlemg12d  40628  cdlemg12e  40629  cdlemg12f  40630  cdlemg12g  40631  cdlemg12  40632  cdlemg13a  40633  cdlemg13  40634  cdlemg17b  40644  cdlemg17f  40648  cdlemg17g  40649  cdlemg17h  40650  cdlemg17pq  40654  cdlemg17  40659  cdlemg19a  40665  cdlemg19  40666  cdlemg21  40668  cdlemg27a  40674  cdlemg27b  40678  cdlemg31c  40681  cdlemg33b0  40683  cdlemg33a  40688  trlcone  40710  cdlemg44  40715  cdlemg48  40719  cdlemk37  40896  cdlemky  40908  cdlemk11ta  40911  cdleml4N  40961  dihord1  41200  dihord2pre2  41208  dihord4  41240  dihord5apre  41244  dihmeetlem1N  41272  dihglblem3N  41277  dihglbcpreN  41282  dihmeetlem3N  41287  dihmeetlem13N  41301  mapdpglem32  41687  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  mzpcong  42960  iscnrm3rlem8  48743