Theorem simp12l 1288

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

Assertion

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

Proof of Theorem simp12l

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

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

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 1089

This theorem is referenced by:  ackbij1lem16  10147  axcontlem4  29050  eqlkr  39559  athgt  39916  llncvrlpln2  40017  4atlem11b  40068  2lnat  40244  cdlemblem  40253  pclfinN  40360  lhp2lt  40461  lhpmcvr5N  40487  lhpmcvr6N  40488  lhp2at0  40492  lhp2atnle  40493  lhp2at0nle  40495  4atexlemex6  40534  cdlemd2  40659  cdlemd7  40664  cdlemd8  40665  cdlemd9  40666  cdleme7aa  40702  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme7  40709  cdleme11c  40721  cdleme11dN  40722  cdleme11e  40723  cdleme11  40730  cdleme14  40733  cdleme15a  40734  cdleme15b  40735  cdleme15d  40737  cdleme15  40738  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme18d  40755  cdleme19b  40764  cdleme19e  40767  cdleme20d  40772  cdleme20g  40775  cdleme20h  40776  cdleme20i  40777  cdleme20j  40778  cdleme20l2  40781  cdleme20l  40782  cdleme20m  40783  cdleme21c  40787  cdleme21ct  40789  cdleme21d  40790  cdleme21e  40791  cdleme22cN  40802  cdleme22f  40806  cdleme22f2  40807  cdleme23a  40809  cdleme23b  40810  cdleme23c  40811  cdleme25a  40813  cdleme25dN  40816  cdleme26fALTN  40822  cdleme26f  40823  cdleme26f2ALTN  40824  cdleme26f2  40825  cdlemefr29bpre0N  40866  cdlemefr29clN  40867  cdlemefr32fvaN  40869  cdlemefr32fva1  40870  cdleme41sn3a  40893  cdleme32le  40907  cdleme35a  40908  cdleme35fnpq  40909  cdleme35b  40910  cdleme35c  40911  cdleme35d  40912  cdleme35e  40913  cdleme35f  40914  cdleme36a  40920  cdleme37m  40922  cdleme39n  40926  cdleme43bN  40950  cdleme43dN  40952  cdleme17d2  40955  cdlemeg46c  40973  cdlemeg46nlpq  40977  cdlemeg46ngfr  40978  cdlemeg46req  40989  cdlemeg46gfv  40990  cdleme50trn1  41009  cdleme50trn2a  41010  cdlemf1  41021  trlord  41029  cdlemb3  41066  cdlemg7fvbwN  41067  cdlemg7aN  41085  cdlemg10a  41100  cdlemg10  41101  cdlemg12d  41106  cdlemg12e  41107  cdlemg12f  41108  cdlemg12g  41109  cdlemg12  41110  cdlemg13a  41111  cdlemg13  41112  cdlemg17b  41122  cdlemg17f  41126  cdlemg17g  41127  cdlemg17h  41128  cdlemg17pq  41132  cdlemg17  41137  cdlemg19a  41143  cdlemg19  41144  cdlemg21  41146  cdlemg27a  41152  cdlemg27b  41156  cdlemg31c  41159  cdlemg33b0  41161  cdlemg33a  41166  trlcone  41188  cdlemg44  41193  cdlemg48  41197  cdlemk37  41374  cdlemky  41386  cdlemk11ta  41389  cdleml4N  41439  dihord1  41678  dihord2pre2  41686  dihord4  41718  dihord5apre  41722  dihmeetlem1N  41750  dihglblem3N  41755  dihglbcpreN  41760  dihmeetlem3N  41765  dihmeetlem13N  41779  mapdpglem32  42165  baerlem3lem2  42170  baerlem5alem2  42171  baerlem5blem2  42172  mzpcong  43418  iscnrm3rlem8  49434