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  10194  axcontlem4  28901  eqlkr  39099  athgt  39457  llncvrlpln2  39558  4atlem11b  39609  2lnat  39785  cdlemblem  39794  pclfinN  39901  lhp2lt  40002  lhpmcvr5N  40028  lhpmcvr6N  40029  lhp2at0  40033  lhp2atnle  40034  lhp2at0nle  40036  4atexlemex6  40075  cdlemd2  40200  cdlemd7  40205  cdlemd8  40206  cdlemd9  40207  cdleme7aa  40243  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme7  40250  cdleme11c  40262  cdleme11dN  40263  cdleme11e  40264  cdleme11  40271  cdleme14  40274  cdleme15a  40275  cdleme15b  40276  cdleme15d  40278  cdleme15  40279  cdleme16b  40280  cdleme16c  40281  cdleme16d  40282  cdleme18d  40296  cdleme19b  40305  cdleme19e  40308  cdleme20d  40313  cdleme20g  40316  cdleme20h  40317  cdleme20i  40318  cdleme20j  40319  cdleme20l2  40322  cdleme20l  40323  cdleme20m  40324  cdleme21c  40328  cdleme21ct  40330  cdleme21d  40331  cdleme21e  40332  cdleme22cN  40343  cdleme22f  40347  cdleme22f2  40348  cdleme23a  40350  cdleme23b  40351  cdleme23c  40352  cdleme25a  40354  cdleme25dN  40357  cdleme26fALTN  40363  cdleme26f  40364  cdleme26f2ALTN  40365  cdleme26f2  40366  cdlemefr29bpre0N  40407  cdlemefr29clN  40408  cdlemefr32fvaN  40410  cdlemefr32fva1  40411  cdleme41sn3a  40434  cdleme32le  40448  cdleme35a  40449  cdleme35fnpq  40450  cdleme35b  40451  cdleme35c  40452  cdleme35d  40453  cdleme35e  40454  cdleme35f  40455  cdleme36a  40461  cdleme37m  40463  cdleme39n  40467  cdleme43bN  40491  cdleme43dN  40493  cdleme17d2  40496  cdlemeg46c  40514  cdlemeg46nlpq  40518  cdlemeg46ngfr  40519  cdlemeg46req  40530  cdlemeg46gfv  40531  cdleme50trn1  40550  cdleme50trn2a  40551  cdlemf1  40562  trlord  40570  cdlemb3  40607  cdlemg7fvbwN  40608  cdlemg7aN  40626  cdlemg10a  40641  cdlemg10  40642  cdlemg12d  40647  cdlemg12e  40648  cdlemg12f  40649  cdlemg12g  40650  cdlemg12  40651  cdlemg13a  40652  cdlemg13  40653  cdlemg17b  40663  cdlemg17f  40667  cdlemg17g  40668  cdlemg17h  40669  cdlemg17pq  40673  cdlemg17  40678  cdlemg19a  40684  cdlemg19  40685  cdlemg21  40687  cdlemg27a  40693  cdlemg27b  40697  cdlemg31c  40700  cdlemg33b0  40702  cdlemg33a  40707  trlcone  40729  cdlemg44  40734  cdlemg48  40738  cdlemk37  40915  cdlemky  40927  cdlemk11ta  40930  cdleml4N  40980  dihord1  41219  dihord2pre2  41227  dihord4  41259  dihord5apre  41263  dihmeetlem1N  41291  dihglblem3N  41296  dihglbcpreN  41301  dihmeetlem3N  41306  dihmeetlem13N  41320  mapdpglem32  41706  baerlem3lem2  41711  baerlem5alem2  41712  baerlem5blem2  41713  mzpcong  42968  iscnrm3rlem8  48939