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  10240  axcontlem4  29432  eqlkr  39980  athgt  40337  llncvrlpln2  40438  4atlem11b  40489  2lnat  40665  cdlemblem  40674  pclfinN  40781  lhp2lt  40882  lhpmcvr5N  40908  lhpmcvr6N  40909  lhp2at0  40913  lhp2atnle  40914  lhp2at0nle  40916  4atexlemex6  40955  cdlemd2  41080  cdlemd7  41085  cdlemd8  41086  cdlemd9  41087  cdleme7aa  41123  cdleme7c  41126  cdleme7d  41127  cdleme7e  41128  cdleme7ga  41129  cdleme7  41130  cdleme11c  41142  cdleme11dN  41143  cdleme11e  41144  cdleme11  41151  cdleme14  41154  cdleme15a  41155  cdleme15b  41156  cdleme15d  41158  cdleme15  41159  cdleme16b  41160  cdleme16c  41161  cdleme16d  41162  cdleme18d  41176  cdleme19b  41185  cdleme19e  41188  cdleme20d  41193  cdleme20g  41196  cdleme20h  41197  cdleme20i  41198  cdleme20j  41199  cdleme20l2  41202  cdleme20l  41203  cdleme20m  41204  cdleme21c  41208  cdleme21ct  41210  cdleme21d  41211  cdleme21e  41212  cdleme22cN  41223  cdleme22f  41227  cdleme22f2  41228  cdleme23a  41230  cdleme23b  41231  cdleme23c  41232  cdleme25a  41234  cdleme25dN  41237  cdleme26fALTN  41243  cdleme26f  41244  cdleme26f2ALTN  41245  cdleme26f2  41246  cdlemefr29bpre0N  41287  cdlemefr29clN  41288  cdlemefr32fvaN  41290  cdlemefr32fva1  41291  cdleme41sn3a  41314  cdleme32le  41328  cdleme35a  41329  cdleme35fnpq  41330  cdleme35b  41331  cdleme35c  41332  cdleme35d  41333  cdleme35e  41334  cdleme35f  41335  cdleme36a  41341  cdleme37m  41343  cdleme39n  41347  cdleme43bN  41371  cdleme43dN  41373  cdleme17d2  41376  cdlemeg46c  41394  cdlemeg46nlpq  41398  cdlemeg46ngfr  41399  cdlemeg46req  41410  cdlemeg46gfv  41411  cdleme50trn1  41430  cdleme50trn2a  41431  cdlemf1  41442  trlord  41450  cdlemb3  41487  cdlemg7fvbwN  41488  cdlemg7aN  41506  cdlemg10a  41521  cdlemg10  41522  cdlemg12d  41527  cdlemg12e  41528  cdlemg12f  41529  cdlemg12g  41530  cdlemg12  41531  cdlemg13a  41532  cdlemg13  41533  cdlemg17b  41543  cdlemg17f  41547  cdlemg17g  41548  cdlemg17h  41549  cdlemg17pq  41553  cdlemg17  41558  cdlemg19a  41564  cdlemg19  41565  cdlemg21  41567  cdlemg27a  41573  cdlemg27b  41577  cdlemg31c  41580  cdlemg33b0  41582  cdlemg33a  41587  trlcone  41609  cdlemg44  41614  cdlemg48  41618  cdlemk37  41795  cdlemky  41807  cdlemk11ta  41810  cdleml4N  41860  dihord1  42099  dihord2pre2  42107  dihord4  42139  dihord5apre  42143  dihmeetlem1N  42171  dihglblem3N  42176  dihglbcpreN  42181  dihmeetlem3N  42186  dihmeetlem13N  42200  mapdpglem32  42586  baerlem3lem2  42591  baerlem5alem2  42592  baerlem5blem2  42593  mzpcong  43821  iscnrm3rlem8  49881