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 394   ∧ 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 395  df-3an 1087

This theorem is referenced by:  ackbij1lem16  10232  axcontlem4  28492  eqlkr  38272  athgt  38630  llncvrlpln2  38731  4atlem11b  38782  2lnat  38958  cdlemblem  38967  pclfinN  39074  lhp2lt  39175  lhpmcvr5N  39201  lhpmcvr6N  39202  lhp2at0  39206  lhp2atnle  39207  lhp2at0nle  39209  4atexlemex6  39248  cdlemd2  39373  cdlemd7  39378  cdlemd8  39379  cdlemd9  39380  cdleme7aa  39416  cdleme7c  39419  cdleme7d  39420  cdleme7e  39421  cdleme7ga  39422  cdleme7  39423  cdleme11c  39435  cdleme11dN  39436  cdleme11e  39437  cdleme11  39444  cdleme14  39447  cdleme15a  39448  cdleme15b  39449  cdleme15d  39451  cdleme15  39452  cdleme16b  39453  cdleme16c  39454  cdleme16d  39455  cdleme18d  39469  cdleme19b  39478  cdleme19e  39481  cdleme20d  39486  cdleme20g  39489  cdleme20h  39490  cdleme20i  39491  cdleme20j  39492  cdleme20l2  39495  cdleme20l  39496  cdleme20m  39497  cdleme21c  39501  cdleme21ct  39503  cdleme21d  39504  cdleme21e  39505  cdleme22cN  39516  cdleme22f  39520  cdleme22f2  39521  cdleme23a  39523  cdleme23b  39524  cdleme23c  39525  cdleme25a  39527  cdleme25dN  39530  cdleme26fALTN  39536  cdleme26f  39537  cdleme26f2ALTN  39538  cdleme26f2  39539  cdlemefr29bpre0N  39580  cdlemefr29clN  39581  cdlemefr32fvaN  39583  cdlemefr32fva1  39584  cdleme41sn3a  39607  cdleme32le  39621  cdleme35a  39622  cdleme35fnpq  39623  cdleme35b  39624  cdleme35c  39625  cdleme35d  39626  cdleme35e  39627  cdleme35f  39628  cdleme36a  39634  cdleme37m  39636  cdleme39n  39640  cdleme43bN  39664  cdleme43dN  39666  cdleme17d2  39669  cdlemeg46c  39687  cdlemeg46nlpq  39691  cdlemeg46ngfr  39692  cdlemeg46req  39703  cdlemeg46gfv  39704  cdleme50trn1  39723  cdleme50trn2a  39724  cdlemf1  39735  trlord  39743  cdlemb3  39780  cdlemg7fvbwN  39781  cdlemg7aN  39799  cdlemg10a  39814  cdlemg10  39815  cdlemg12d  39820  cdlemg12e  39821  cdlemg12f  39822  cdlemg12g  39823  cdlemg12  39824  cdlemg13a  39825  cdlemg13  39826  cdlemg17b  39836  cdlemg17f  39840  cdlemg17g  39841  cdlemg17h  39842  cdlemg17pq  39846  cdlemg17  39851  cdlemg19a  39857  cdlemg19  39858  cdlemg21  39860  cdlemg27a  39866  cdlemg27b  39870  cdlemg31c  39873  cdlemg33b0  39875  cdlemg33a  39880  trlcone  39902  cdlemg44  39907  cdlemg48  39911  cdlemk37  40088  cdlemky  40100  cdlemk11ta  40103  cdleml4N  40153  dihord1  40392  dihord2pre2  40400  dihord4  40432  dihord5apre  40436  dihmeetlem1N  40464  dihglblem3N  40469  dihglbcpreN  40474  dihmeetlem3N  40479  dihmeetlem13N  40493  mapdpglem32  40879  baerlem3lem2  40884  baerlem5alem2  40885  baerlem5blem2  40886  mzpcong  42013  iscnrm3rlem8  47667