Theorem simp21l 1297

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

Assertion

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

Proof of Theorem simp21l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  modexp  14198  segconeu  36246  4atlem10  40105  lplncvrlvol2  40114  4atex  40575  4atex2-0cOLDN  40579  cdlemd2  40698  cdlemd3  40699  cdlemd4  40700  cdleme0e  40716  cdleme0moN  40724  cdleme3g  40733  cdleme3h  40734  cdleme3  40736  cdleme9  40752  cdleme11c  40760  cdleme11dN  40761  cdleme11e  40762  cdleme11fN  40763  cdleme11h  40765  cdleme11j  40766  cdleme11k  40767  cdleme11  40769  cdleme12  40770  cdleme13  40771  cdleme14  40772  cdleme15a  40773  cdleme15b  40774  cdleme15c  40775  cdleme15d  40776  cdleme15  40777  cdleme16b  40778  cdleme16c  40779  cdleme16d  40780  cdleme16e  40781  cdleme16f  40782  cdleme17d1  40788  cdleme18a  40790  cdleme18b  40791  cdleme18c  40792  cdleme18d  40794  cdleme19b  40803  cdleme19d  40805  cdleme19e  40806  cdleme20c  40810  cdleme20d  40811  cdleme20e  40812  cdleme20f  40813  cdleme20g  40814  cdleme20h  40815  cdleme20j  40817  cdleme20l2  40820  cdleme20l  40821  cdleme20m  40822  cdleme20  40823  cdleme21ct  40828  cdleme21e  40830  cdleme21i  40834  cdleme22aa  40838  cdleme22cN  40841  cdleme22d  40842  cdleme22e  40843  cdleme22eALTN  40844  cdleme22f  40845  cdleme26e  40858  cdleme27a  40866  cdleme32e  40944  cdlemg2fv2  41099  cdlemg4a  41107  cdlemg4d  41112  cdlemg4  41116  cdlemg6c  41119  cdlemg8b  41127  cdlemg8c  41128  cdlemg9a  41131  cdlemg9  41133  cdlemg12a  41142  cdlemg12c  41144  cdlemg17dALTN  41163  cdlemg17h  41167  cdlemg18b  41178  cdlemg18c  41179  cdlemg18d  41180  cdlemg18  41181  cdlemg19a  41182  cdlemg21  41185  cdlemg28a  41192  cdlemg31b0a  41194  cdlemg31d  41199  cdlemg33b0  41200  cdlemg33a  41205  cdlemh  41316  cdlemk5  41335  cdlemk6  41336  cdlemk7  41347  cdlemk11  41348  cdlemk12  41349  cdlemk21N  41372  cdlemk20  41373  cdlemk28-3  41407  cdlemk34  41409  cdlemkfid3N  41424  cdlemk35s-id  41437  cdlemk39s-id  41439  cdlemk55u1  41464  cdlemn2  41694  cdlemn10  41705  dihjustlem  41715