Theorem simp12l 1284

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

Assertion

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

Proof of Theorem simp12l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  ackbij1lem16  10252  axcontlem4  28771  eqlkr  38560  athgt  38918  llncvrlpln2  39019  4atlem11b  39070  2lnat  39246  cdlemblem  39255  pclfinN  39362  lhp2lt  39463  lhpmcvr5N  39489  lhpmcvr6N  39490  lhp2at0  39494  lhp2atnle  39495  lhp2at0nle  39497  4atexlemex6  39536  cdlemd2  39661  cdlemd7  39666  cdlemd8  39667  cdlemd9  39668  cdleme7aa  39704  cdleme7c  39707  cdleme7d  39708  cdleme7e  39709  cdleme7ga  39710  cdleme7  39711  cdleme11c  39723  cdleme11dN  39724  cdleme11e  39725  cdleme11  39732  cdleme14  39735  cdleme15a  39736  cdleme15b  39737  cdleme15d  39739  cdleme15  39740  cdleme16b  39741  cdleme16c  39742  cdleme16d  39743  cdleme18d  39757  cdleme19b  39766  cdleme19e  39769  cdleme20d  39774  cdleme20g  39777  cdleme20h  39778  cdleme20i  39779  cdleme20j  39780  cdleme20l2  39783  cdleme20l  39784  cdleme20m  39785  cdleme21c  39789  cdleme21ct  39791  cdleme21d  39792  cdleme21e  39793  cdleme22cN  39804  cdleme22f  39808  cdleme22f2  39809  cdleme23a  39811  cdleme23b  39812  cdleme23c  39813  cdleme25a  39815  cdleme25dN  39818  cdleme26fALTN  39824  cdleme26f  39825  cdleme26f2ALTN  39826  cdleme26f2  39827  cdlemefr29bpre0N  39868  cdlemefr29clN  39869  cdlemefr32fvaN  39871  cdlemefr32fva1  39872  cdleme41sn3a  39895  cdleme32le  39909  cdleme35a  39910  cdleme35fnpq  39911  cdleme35b  39912  cdleme35c  39913  cdleme35d  39914  cdleme35e  39915  cdleme35f  39916  cdleme36a  39922  cdleme37m  39924  cdleme39n  39928  cdleme43bN  39952  cdleme43dN  39954  cdleme17d2  39957  cdlemeg46c  39975  cdlemeg46nlpq  39979  cdlemeg46ngfr  39980  cdlemeg46req  39991  cdlemeg46gfv  39992  cdleme50trn1  40011  cdleme50trn2a  40012  cdlemf1  40023  trlord  40031  cdlemb3  40068  cdlemg7fvbwN  40069  cdlemg7aN  40087  cdlemg10a  40102  cdlemg10  40103  cdlemg12d  40108  cdlemg12e  40109  cdlemg12f  40110  cdlemg12g  40111  cdlemg12  40112  cdlemg13a  40113  cdlemg13  40114  cdlemg17b  40124  cdlemg17f  40128  cdlemg17g  40129  cdlemg17h  40130  cdlemg17pq  40134  cdlemg17  40139  cdlemg19a  40145  cdlemg19  40146  cdlemg21  40148  cdlemg27a  40154  cdlemg27b  40158  cdlemg31c  40161  cdlemg33b0  40163  cdlemg33a  40168  trlcone  40190  cdlemg44  40195  cdlemg48  40199  cdlemk37  40376  cdlemky  40388  cdlemk11ta  40391  cdleml4N  40441  dihord1  40680  dihord2pre2  40688  dihord4  40720  dihord5apre  40724  dihmeetlem1N  40752  dihglblem3N  40757  dihglbcpreN  40762  dihmeetlem3N  40767  dihmeetlem13N  40781  mapdpglem32  41167  baerlem3lem2  41172  baerlem5alem2  41173  baerlem5blem2  41174  mzpcong  42365  iscnrm3rlem8  47938