Theorem simp21l 1288

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

Assertion

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

Proof of Theorem simp21l

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

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

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 396  df-3an 1087

This theorem is referenced by:  modexp  13881  segconeu  34240  4atlem10  37547  lplncvrlvol2  37556  4atex  38017  4atex2-0cOLDN  38021  cdlemd2  38140  cdlemd3  38141  cdlemd4  38142  cdleme0e  38158  cdleme0moN  38166  cdleme3g  38175  cdleme3h  38176  cdleme3  38178  cdleme9  38194  cdleme11c  38202  cdleme11dN  38203  cdleme11e  38204  cdleme11fN  38205  cdleme11h  38207  cdleme11j  38208  cdleme11k  38209  cdleme11  38211  cdleme12  38212  cdleme13  38213  cdleme14  38214  cdleme15a  38215  cdleme15b  38216  cdleme15c  38217  cdleme15d  38218  cdleme15  38219  cdleme16b  38220  cdleme16c  38221  cdleme16d  38222  cdleme16e  38223  cdleme16f  38224  cdleme17d1  38230  cdleme18a  38232  cdleme18b  38233  cdleme18c  38234  cdleme18d  38236  cdleme19b  38245  cdleme19d  38247  cdleme19e  38248  cdleme20c  38252  cdleme20d  38253  cdleme20e  38254  cdleme20f  38255  cdleme20g  38256  cdleme20h  38257  cdleme20j  38259  cdleme20l2  38262  cdleme20l  38263  cdleme20m  38264  cdleme20  38265  cdleme21ct  38270  cdleme21e  38272  cdleme21i  38276  cdleme22aa  38280  cdleme22cN  38283  cdleme22d  38284  cdleme22e  38285  cdleme22eALTN  38286  cdleme22f  38287  cdleme26e  38300  cdleme27a  38308  cdleme32e  38386  cdlemg2fv2  38541  cdlemg4a  38549  cdlemg4d  38554  cdlemg4  38558  cdlemg6c  38561  cdlemg8b  38569  cdlemg8c  38570  cdlemg9a  38573  cdlemg9  38575  cdlemg12a  38584  cdlemg12c  38586  cdlemg17dALTN  38605  cdlemg17h  38609  cdlemg18b  38620  cdlemg18c  38621  cdlemg18d  38622  cdlemg18  38623  cdlemg19a  38624  cdlemg21  38627  cdlemg28a  38634  cdlemg31b0a  38636  cdlemg31d  38641  cdlemg33b0  38642  cdlemg33a  38647  cdlemh  38758  cdlemk5  38777  cdlemk6  38778  cdlemk7  38789  cdlemk11  38790  cdlemk12  38791  cdlemk21N  38814  cdlemk20  38815  cdlemk28-3  38849  cdlemk34  38851  cdlemkfid3N  38866  cdlemk35s-id  38879  cdlemk39s-id  38881  cdlemk55u1  38906  cdlemn2  39136  cdlemn10  39147  dihjustlem  39157