Theorem simp12l 1305

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

Assertion

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

Proof of Theorem simp12l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ackbij1lem16  10315  axcontlem4  29550  eqlkr  40249  athgt  40606  llncvrlpln2  40707  4atlem11b  40758  2lnat  40934  cdlemblem  40943  pclfinN  41050  lhp2lt  41151  lhpmcvr5N  41177  lhpmcvr6N  41178  lhp2at0  41182  lhp2atnle  41183  lhp2at0nle  41185  4atexlemex6  41224  cdlemd2  41349  cdlemd7  41354  cdlemd8  41355  cdlemd9  41356  cdleme7aa  41392  cdleme7c  41395  cdleme7d  41396  cdleme7e  41397  cdleme7ga  41398  cdleme7  41399  cdleme11c  41411  cdleme11dN  41412  cdleme11e  41413  cdleme11  41420  cdleme14  41423  cdleme15a  41424  cdleme15b  41425  cdleme15d  41427  cdleme15  41428  cdleme16b  41429  cdleme16c  41430  cdleme16d  41431  cdleme18d  41445  cdleme19b  41454  cdleme19e  41457  cdleme20d  41462  cdleme20g  41465  cdleme20h  41466  cdleme20i  41467  cdleme20j  41468  cdleme20l2  41471  cdleme20l  41472  cdleme20m  41473  cdleme21c  41477  cdleme21ct  41479  cdleme21d  41480  cdleme21e  41481  cdleme22cN  41492  cdleme22f  41496  cdleme22f2  41497  cdleme23a  41499  cdleme23b  41500  cdleme23c  41501  cdleme25a  41503  cdleme25dN  41506  cdleme26fALTN  41512  cdleme26f  41513  cdleme26f2ALTN  41514  cdleme26f2  41515  cdlemefr29bpre0N  41556  cdlemefr29clN  41557  cdlemefr32fvaN  41559  cdlemefr32fva1  41560  cdleme41sn3a  41583  cdleme32le  41597  cdleme35a  41598  cdleme35fnpq  41599  cdleme35b  41600  cdleme35c  41601  cdleme35d  41602  cdleme35e  41603  cdleme35f  41604  cdleme36a  41610  cdleme37m  41612  cdleme39n  41616  cdleme43bN  41640  cdleme43dN  41642  cdleme17d2  41645  cdlemeg46c  41663  cdlemeg46nlpq  41667  cdlemeg46ngfr  41668  cdlemeg46req  41679  cdlemeg46gfv  41680  cdleme50trn1  41699  cdleme50trn2a  41700  cdlemf1  41711  trlord  41719  cdlemb3  41756  cdlemg7fvbwN  41757  cdlemg7aN  41775  cdlemg10a  41790  cdlemg10  41791  cdlemg12d  41796  cdlemg12e  41797  cdlemg12f  41798  cdlemg12g  41799  cdlemg12  41800  cdlemg13a  41801  cdlemg13  41802  cdlemg17b  41812  cdlemg17f  41816  cdlemg17g  41817  cdlemg17h  41818  cdlemg17pq  41822  cdlemg17  41827  cdlemg19a  41833  cdlemg19  41834  cdlemg21  41836  cdlemg27a  41842  cdlemg27b  41846  cdlemg31c  41849  cdlemg33b0  41851  cdlemg33a  41856  trlcone  41878  cdlemg44  41883  cdlemg48  41887  cdlemk37  42064  cdlemky  42076  cdlemk11ta  42079  cdleml4N  42129  dihord1  42368  dihord2pre2  42376  dihord4  42408  dihord5apre  42412  dihmeetlem1N  42440  dihglblem3N  42445  dihglbcpreN  42450  dihmeetlem3N  42455  dihmeetlem13N  42469  mapdpglem32  42855  baerlem3lem2  42860  baerlem5alem2  42861  baerlem5blem2  42862  mzpcong  44072  iscnrm3rlem8  50154