Theorem simp12l 1303

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

Assertion

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

Proof of Theorem simp12l

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  ackbij1lem16  10205  axcontlem4  29226  eqlkr  39735  athgt  40092  llncvrlpln2  40193  4atlem11b  40244  2lnat  40420  cdlemblem  40429  pclfinN  40536  lhp2lt  40637  lhpmcvr5N  40663  lhpmcvr6N  40664  lhp2at0  40668  lhp2atnle  40669  lhp2at0nle  40671  4atexlemex6  40710  cdlemd2  40835  cdlemd7  40840  cdlemd8  40841  cdlemd9  40842  cdleme7aa  40878  cdleme7c  40881  cdleme7d  40882  cdleme7e  40883  cdleme7ga  40884  cdleme7  40885  cdleme11c  40897  cdleme11dN  40898  cdleme11e  40899  cdleme11  40906  cdleme14  40909  cdleme15a  40910  cdleme15b  40911  cdleme15d  40913  cdleme15  40914  cdleme16b  40915  cdleme16c  40916  cdleme16d  40917  cdleme18d  40931  cdleme19b  40940  cdleme19e  40943  cdleme20d  40948  cdleme20g  40951  cdleme20h  40952  cdleme20i  40953  cdleme20j  40954  cdleme20l2  40957  cdleme20l  40958  cdleme20m  40959  cdleme21c  40963  cdleme21ct  40965  cdleme21d  40966  cdleme21e  40967  cdleme22cN  40978  cdleme22f  40982  cdleme22f2  40983  cdleme23a  40985  cdleme23b  40986  cdleme23c  40987  cdleme25a  40989  cdleme25dN  40992  cdleme26fALTN  40998  cdleme26f  40999  cdleme26f2ALTN  41000  cdleme26f2  41001  cdlemefr29bpre0N  41042  cdlemefr29clN  41043  cdlemefr32fvaN  41045  cdlemefr32fva1  41046  cdleme41sn3a  41069  cdleme32le  41083  cdleme35a  41084  cdleme35fnpq  41085  cdleme35b  41086  cdleme35c  41087  cdleme35d  41088  cdleme35e  41089  cdleme35f  41090  cdleme36a  41096  cdleme37m  41098  cdleme39n  41102  cdleme43bN  41126  cdleme43dN  41128  cdleme17d2  41131  cdlemeg46c  41149  cdlemeg46nlpq  41153  cdlemeg46ngfr  41154  cdlemeg46req  41165  cdlemeg46gfv  41166  cdleme50trn1  41185  cdleme50trn2a  41186  cdlemf1  41197  trlord  41205  cdlemb3  41242  cdlemg7fvbwN  41243  cdlemg7aN  41261  cdlemg10a  41276  cdlemg10  41277  cdlemg12d  41282  cdlemg12e  41283  cdlemg12f  41284  cdlemg12g  41285  cdlemg12  41286  cdlemg13a  41287  cdlemg13  41288  cdlemg17b  41298  cdlemg17f  41302  cdlemg17g  41303  cdlemg17h  41304  cdlemg17pq  41308  cdlemg17  41313  cdlemg19a  41319  cdlemg19  41320  cdlemg21  41322  cdlemg27a  41328  cdlemg27b  41332  cdlemg31c  41335  cdlemg33b0  41337  cdlemg33a  41342  trlcone  41364  cdlemg44  41369  cdlemg48  41373  cdlemk37  41550  cdlemky  41562  cdlemk11ta  41565  cdleml4N  41615  dihord1  41854  dihord2pre2  41862  dihord4  41894  dihord5apre  41898  dihmeetlem1N  41926  dihglblem3N  41931  dihglbcpreN  41936  dihmeetlem3N  41941  dihmeetlem13N  41955  mapdpglem32  42341  baerlem3lem2  42346  baerlem5alem2  42347  baerlem5blem2  42348  mzpcong  43561  iscnrm3rlem8  49576