Theorem simp12l 1287

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

Assertion

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

Proof of Theorem simp12l

Step	Hyp	Ref	Expression
1		simp2l 1200	. 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  10274  axcontlem4  28982  eqlkr  39100  athgt  39458  llncvrlpln2  39559  4atlem11b  39610  2lnat  39786  cdlemblem  39795  pclfinN  39902  lhp2lt  40003  lhpmcvr5N  40029  lhpmcvr6N  40030  lhp2at0  40034  lhp2atnle  40035  lhp2at0nle  40037  4atexlemex6  40076  cdlemd2  40201  cdlemd7  40206  cdlemd8  40207  cdlemd9  40208  cdleme7aa  40244  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme7  40251  cdleme11c  40263  cdleme11dN  40264  cdleme11e  40265  cdleme11  40272  cdleme14  40275  cdleme15a  40276  cdleme15b  40277  cdleme15d  40279  cdleme15  40280  cdleme16b  40281  cdleme16c  40282  cdleme16d  40283  cdleme18d  40297  cdleme19b  40306  cdleme19e  40309  cdleme20d  40314  cdleme20g  40317  cdleme20h  40318  cdleme20i  40319  cdleme20j  40320  cdleme20l2  40323  cdleme20l  40324  cdleme20m  40325  cdleme21c  40329  cdleme21ct  40331  cdleme21d  40332  cdleme21e  40333  cdleme22cN  40344  cdleme22f  40348  cdleme22f2  40349  cdleme23a  40351  cdleme23b  40352  cdleme23c  40353  cdleme25a  40355  cdleme25dN  40358  cdleme26fALTN  40364  cdleme26f  40365  cdleme26f2ALTN  40366  cdleme26f2  40367  cdlemefr29bpre0N  40408  cdlemefr29clN  40409  cdlemefr32fvaN  40411  cdlemefr32fva1  40412  cdleme41sn3a  40435  cdleme32le  40449  cdleme35a  40450  cdleme35fnpq  40451  cdleme35b  40452  cdleme35c  40453  cdleme35d  40454  cdleme35e  40455  cdleme35f  40456  cdleme36a  40462  cdleme37m  40464  cdleme39n  40468  cdleme43bN  40492  cdleme43dN  40494  cdleme17d2  40497  cdlemeg46c  40515  cdlemeg46nlpq  40519  cdlemeg46ngfr  40520  cdlemeg46req  40531  cdlemeg46gfv  40532  cdleme50trn1  40551  cdleme50trn2a  40552  cdlemf1  40563  trlord  40571  cdlemb3  40608  cdlemg7fvbwN  40609  cdlemg7aN  40627  cdlemg10a  40642  cdlemg10  40643  cdlemg12d  40648  cdlemg12e  40649  cdlemg12f  40650  cdlemg12g  40651  cdlemg12  40652  cdlemg13a  40653  cdlemg13  40654  cdlemg17b  40664  cdlemg17f  40668  cdlemg17g  40669  cdlemg17h  40670  cdlemg17pq  40674  cdlemg17  40679  cdlemg19a  40685  cdlemg19  40686  cdlemg21  40688  cdlemg27a  40694  cdlemg27b  40698  cdlemg31c  40701  cdlemg33b0  40703  cdlemg33a  40708  trlcone  40730  cdlemg44  40735  cdlemg48  40739  cdlemk37  40916  cdlemky  40928  cdlemk11ta  40931  cdleml4N  40981  dihord1  41220  dihord2pre2  41228  dihord4  41260  dihord5apre  41264  dihmeetlem1N  41292  dihglblem3N  41297  dihglbcpreN  41302  dihmeetlem3N  41307  dihmeetlem13N  41321  mapdpglem32  41707  baerlem3lem2  41712  baerlem5alem2  41713  baerlem5blem2  41714  mzpcong  42984  iscnrm3rlem8  48844