Theorem simp21l 1289

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

Assertion

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

Proof of Theorem simp21l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  modexp  13953  segconeu  34313  4atlem10  37620  lplncvrlvol2  37629  4atex  38090  4atex2-0cOLDN  38094  cdlemd2  38213  cdlemd3  38214  cdlemd4  38215  cdleme0e  38231  cdleme0moN  38239  cdleme3g  38248  cdleme3h  38249  cdleme3  38251  cdleme9  38267  cdleme11c  38275  cdleme11dN  38276  cdleme11e  38277  cdleme11fN  38278  cdleme11h  38280  cdleme11j  38281  cdleme11k  38282  cdleme11  38284  cdleme12  38285  cdleme13  38286  cdleme14  38287  cdleme15a  38288  cdleme15b  38289  cdleme15c  38290  cdleme15d  38291  cdleme15  38292  cdleme16b  38293  cdleme16c  38294  cdleme16d  38295  cdleme16e  38296  cdleme16f  38297  cdleme17d1  38303  cdleme18a  38305  cdleme18b  38306  cdleme18c  38307  cdleme18d  38309  cdleme19b  38318  cdleme19d  38320  cdleme19e  38321  cdleme20c  38325  cdleme20d  38326  cdleme20e  38327  cdleme20f  38328  cdleme20g  38329  cdleme20h  38330  cdleme20j  38332  cdleme20l2  38335  cdleme20l  38336  cdleme20m  38337  cdleme20  38338  cdleme21ct  38343  cdleme21e  38345  cdleme21i  38349  cdleme22aa  38353  cdleme22cN  38356  cdleme22d  38357  cdleme22e  38358  cdleme22eALTN  38359  cdleme22f  38360  cdleme26e  38373  cdleme27a  38381  cdleme32e  38459  cdlemg2fv2  38614  cdlemg4a  38622  cdlemg4d  38627  cdlemg4  38631  cdlemg6c  38634  cdlemg8b  38642  cdlemg8c  38643  cdlemg9a  38646  cdlemg9  38648  cdlemg12a  38657  cdlemg12c  38659  cdlemg17dALTN  38678  cdlemg17h  38682  cdlemg18b  38693  cdlemg18c  38694  cdlemg18d  38695  cdlemg18  38696  cdlemg19a  38697  cdlemg21  38700  cdlemg28a  38707  cdlemg31b0a  38709  cdlemg31d  38714  cdlemg33b0  38715  cdlemg33a  38720  cdlemh  38831  cdlemk5  38850  cdlemk6  38851  cdlemk7  38862  cdlemk11  38863  cdlemk12  38864  cdlemk21N  38887  cdlemk20  38888  cdlemk28-3  38922  cdlemk34  38924  cdlemkfid3N  38939  cdlemk35s-id  38952  cdlemk39s-id  38954  cdlemk55u1  38979  cdlemn2  39209  cdlemn10  39220  dihjustlem  39230