Theorem simp21l 1292

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

Assertion

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

Proof of Theorem simp21l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 400  df-3an 1091

This theorem is referenced by:  modexp  13770  segconeu  33999  4atlem10  37306  lplncvrlvol2  37315  4atex  37776  4atex2-0cOLDN  37780  cdlemd2  37899  cdlemd3  37900  cdlemd4  37901  cdleme0e  37917  cdleme0moN  37925  cdleme3g  37934  cdleme3h  37935  cdleme3  37937  cdleme9  37953  cdleme11c  37961  cdleme11dN  37962  cdleme11e  37963  cdleme11fN  37964  cdleme11h  37966  cdleme11j  37967  cdleme11k  37968  cdleme11  37970  cdleme12  37971  cdleme13  37972  cdleme14  37973  cdleme15a  37974  cdleme15b  37975  cdleme15c  37976  cdleme15d  37977  cdleme15  37978  cdleme16b  37979  cdleme16c  37980  cdleme16d  37981  cdleme16e  37982  cdleme16f  37983  cdleme17d1  37989  cdleme18a  37991  cdleme18b  37992  cdleme18c  37993  cdleme18d  37995  cdleme19b  38004  cdleme19d  38006  cdleme19e  38007  cdleme20c  38011  cdleme20d  38012  cdleme20e  38013  cdleme20f  38014  cdleme20g  38015  cdleme20h  38016  cdleme20j  38018  cdleme20l2  38021  cdleme20l  38022  cdleme20m  38023  cdleme20  38024  cdleme21ct  38029  cdleme21e  38031  cdleme21i  38035  cdleme22aa  38039  cdleme22cN  38042  cdleme22d  38043  cdleme22e  38044  cdleme22eALTN  38045  cdleme22f  38046  cdleme26e  38059  cdleme27a  38067  cdleme32e  38145  cdlemg2fv2  38300  cdlemg4a  38308  cdlemg4d  38313  cdlemg4  38317  cdlemg6c  38320  cdlemg8b  38328  cdlemg8c  38329  cdlemg9a  38332  cdlemg9  38334  cdlemg12a  38343  cdlemg12c  38345  cdlemg17dALTN  38364  cdlemg17h  38368  cdlemg18b  38379  cdlemg18c  38380  cdlemg18d  38381  cdlemg18  38382  cdlemg19a  38383  cdlemg21  38386  cdlemg28a  38393  cdlemg31b0a  38395  cdlemg31d  38400  cdlemg33b0  38401  cdlemg33a  38406  cdlemh  38517  cdlemk5  38536  cdlemk6  38537  cdlemk7  38548  cdlemk11  38549  cdlemk12  38550  cdlemk21N  38573  cdlemk20  38574  cdlemk28-3  38608  cdlemk34  38610  cdlemkfid3N  38625  cdlemk35s-id  38638  cdlemk39s-id  38640  cdlemk55u1  38665  cdlemn2  38895  cdlemn10  38906  dihjustlem  38916