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 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)

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

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 1105

This theorem is referenced by:  ackbij1lem16  10218  axcontlem4  29295  eqlkr  39851  athgt  40208  llncvrlpln2  40309  4atlem11b  40360  2lnat  40536  cdlemblem  40545  pclfinN  40652  lhp2lt  40753  lhpmcvr5N  40779  lhpmcvr6N  40780  lhp2at0  40784  lhp2atnle  40785  lhp2at0nle  40787  4atexlemex6  40826  cdlemd2  40951  cdlemd7  40956  cdlemd8  40957  cdlemd9  40958  cdleme7aa  40994  cdleme7c  40997  cdleme7d  40998  cdleme7e  40999  cdleme7ga  41000  cdleme7  41001  cdleme11c  41013  cdleme11dN  41014  cdleme11e  41015  cdleme11  41022  cdleme14  41025  cdleme15a  41026  cdleme15b  41027  cdleme15d  41029  cdleme15  41030  cdleme16b  41031  cdleme16c  41032  cdleme16d  41033  cdleme18d  41047  cdleme19b  41056  cdleme19e  41059  cdleme20d  41064  cdleme20g  41067  cdleme20h  41068  cdleme20i  41069  cdleme20j  41070  cdleme20l2  41073  cdleme20l  41074  cdleme20m  41075  cdleme21c  41079  cdleme21ct  41081  cdleme21d  41082  cdleme21e  41083  cdleme22cN  41094  cdleme22f  41098  cdleme22f2  41099  cdleme23a  41101  cdleme23b  41102  cdleme23c  41103  cdleme25a  41105  cdleme25dN  41108  cdleme26fALTN  41114  cdleme26f  41115  cdleme26f2ALTN  41116  cdleme26f2  41117  cdlemefr29bpre0N  41158  cdlemefr29clN  41159  cdlemefr32fvaN  41161  cdlemefr32fva1  41162  cdleme41sn3a  41185  cdleme32le  41199  cdleme35a  41200  cdleme35fnpq  41201  cdleme35b  41202  cdleme35c  41203  cdleme35d  41204  cdleme35e  41205  cdleme35f  41206  cdleme36a  41212  cdleme37m  41214  cdleme39n  41218  cdleme43bN  41242  cdleme43dN  41244  cdleme17d2  41247  cdlemeg46c  41265  cdlemeg46nlpq  41269  cdlemeg46ngfr  41270  cdlemeg46req  41281  cdlemeg46gfv  41282  cdleme50trn1  41301  cdleme50trn2a  41302  cdlemf1  41313  trlord  41321  cdlemb3  41358  cdlemg7fvbwN  41359  cdlemg7aN  41377  cdlemg10a  41392  cdlemg10  41393  cdlemg12d  41398  cdlemg12e  41399  cdlemg12f  41400  cdlemg12g  41401  cdlemg12  41402  cdlemg13a  41403  cdlemg13  41404  cdlemg17b  41414  cdlemg17f  41418  cdlemg17g  41419  cdlemg17h  41420  cdlemg17pq  41424  cdlemg17  41429  cdlemg19a  41435  cdlemg19  41436  cdlemg21  41438  cdlemg27a  41444  cdlemg27b  41448  cdlemg31c  41451  cdlemg33b0  41453  cdlemg33a  41458  trlcone  41480  cdlemg44  41485  cdlemg48  41489  cdlemk37  41666  cdlemky  41678  cdlemk11ta  41681  cdleml4N  41731  dihord1  41970  dihord2pre2  41978  dihord4  42010  dihord5apre  42014  dihmeetlem1N  42042  dihglblem3N  42047  dihglbcpreN  42052  dihmeetlem3N  42057  dihmeetlem13N  42071  mapdpglem32  42457  baerlem3lem2  42462  baerlem5alem2  42463  baerlem5blem2  42464  mzpcong  43679  iscnrm3rlem8  49702