Theorem simp21l 1291

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

Assertion

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

Proof of Theorem simp21l

Step	Hyp	Ref	Expression
1		simp1l 1198	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant2 1134	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜑)

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

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 1088

This theorem is referenced by:  modexp  14163  segconeu  35984  4atlem10  39585  lplncvrlvol2  39594  4atex  40055  4atex2-0cOLDN  40059  cdlemd2  40178  cdlemd3  40179  cdlemd4  40180  cdleme0e  40196  cdleme0moN  40204  cdleme3g  40213  cdleme3h  40214  cdleme3  40216  cdleme9  40232  cdleme11c  40240  cdleme11dN  40241  cdleme11e  40242  cdleme11fN  40243  cdleme11h  40245  cdleme11j  40246  cdleme11k  40247  cdleme11  40249  cdleme12  40250  cdleme13  40251  cdleme14  40252  cdleme15a  40253  cdleme15b  40254  cdleme15c  40255  cdleme15d  40256  cdleme15  40257  cdleme16b  40258  cdleme16c  40259  cdleme16d  40260  cdleme16e  40261  cdleme16f  40262  cdleme17d1  40268  cdleme18a  40270  cdleme18b  40271  cdleme18c  40272  cdleme18d  40274  cdleme19b  40283  cdleme19d  40285  cdleme19e  40286  cdleme20c  40290  cdleme20d  40291  cdleme20e  40292  cdleme20f  40293  cdleme20g  40294  cdleme20h  40295  cdleme20j  40297  cdleme20l2  40300  cdleme20l  40301  cdleme20m  40302  cdleme20  40303  cdleme21ct  40308  cdleme21e  40310  cdleme21i  40314  cdleme22aa  40318  cdleme22cN  40321  cdleme22d  40322  cdleme22e  40323  cdleme22eALTN  40324  cdleme22f  40325  cdleme26e  40338  cdleme27a  40346  cdleme32e  40424  cdlemg2fv2  40579  cdlemg4a  40587  cdlemg4d  40592  cdlemg4  40596  cdlemg6c  40599  cdlemg8b  40607  cdlemg8c  40608  cdlemg9a  40611  cdlemg9  40613  cdlemg12a  40622  cdlemg12c  40624  cdlemg17dALTN  40643  cdlemg17h  40647  cdlemg18b  40658  cdlemg18c  40659  cdlemg18d  40660  cdlemg18  40661  cdlemg19a  40662  cdlemg21  40665  cdlemg28a  40672  cdlemg31b0a  40674  cdlemg31d  40679  cdlemg33b0  40680  cdlemg33a  40685  cdlemh  40796  cdlemk5  40815  cdlemk6  40816  cdlemk7  40827  cdlemk11  40828  cdlemk12  40829  cdlemk21N  40852  cdlemk20  40853  cdlemk28-3  40887  cdlemk34  40889  cdlemkfid3N  40904  cdlemk35s-id  40917  cdlemk39s-id  40919  cdlemk55u1  40944  cdlemn2  41174  cdlemn10  41185  dihjustlem  41195