Theorem simp21l 1309

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

Assertion

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

Proof of Theorem simp21l

Step	Hyp	Ref	Expression
1		simp1l 1216	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant2 1152	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:  modexp  14276  segconeu  36484  4atlem10  40361  lplncvrlvol2  40370  4atex  40831  4atex2-0cOLDN  40835  cdlemd2  40954  cdlemd3  40955  cdlemd4  40956  cdleme0e  40972  cdleme0moN  40980  cdleme3g  40989  cdleme3h  40990  cdleme3  40992  cdleme9  41008  cdleme11c  41016  cdleme11dN  41017  cdleme11e  41018  cdleme11fN  41019  cdleme11h  41021  cdleme11j  41022  cdleme11k  41023  cdleme11  41025  cdleme12  41026  cdleme13  41027  cdleme14  41028  cdleme15a  41029  cdleme15b  41030  cdleme15c  41031  cdleme15d  41032  cdleme15  41033  cdleme16b  41034  cdleme16c  41035  cdleme16d  41036  cdleme16e  41037  cdleme16f  41038  cdleme17d1  41044  cdleme18a  41046  cdleme18b  41047  cdleme18c  41048  cdleme18d  41050  cdleme19b  41059  cdleme19d  41061  cdleme19e  41062  cdleme20c  41066  cdleme20d  41067  cdleme20e  41068  cdleme20f  41069  cdleme20g  41070  cdleme20h  41071  cdleme20j  41073  cdleme20l2  41076  cdleme20l  41077  cdleme20m  41078  cdleme20  41079  cdleme21ct  41084  cdleme21e  41086  cdleme21i  41090  cdleme22aa  41094  cdleme22cN  41097  cdleme22d  41098  cdleme22e  41099  cdleme22eALTN  41100  cdleme22f  41101  cdleme26e  41114  cdleme27a  41122  cdleme32e  41200  cdlemg2fv2  41355  cdlemg4a  41363  cdlemg4d  41368  cdlemg4  41372  cdlemg6c  41375  cdlemg8b  41383  cdlemg8c  41384  cdlemg9a  41387  cdlemg9  41389  cdlemg12a  41398  cdlemg12c  41400  cdlemg17dALTN  41419  cdlemg17h  41423  cdlemg18b  41434  cdlemg18c  41435  cdlemg18d  41436  cdlemg18  41437  cdlemg19a  41438  cdlemg21  41441  cdlemg28a  41448  cdlemg31b0a  41450  cdlemg31d  41455  cdlemg33b0  41456  cdlemg33a  41461  cdlemh  41572  cdlemk5  41591  cdlemk6  41592  cdlemk7  41603  cdlemk11  41604  cdlemk12  41605  cdlemk21N  41628  cdlemk20  41629  cdlemk28-3  41663  cdlemk34  41665  cdlemkfid3N  41680  cdlemk35s-id  41693  cdlemk39s-id  41695  cdlemk55u1  41720  cdlemn2  41950  cdlemn10  41961  dihjustlem  41971