Theorem simp21r 1290

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

Assertion

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

Proof of Theorem simp21r

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

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

This theorem is referenced by:  modexp  14274  segconeu  35993  4atlem10  39589  lplncvrlvol2  39598  4atex  40059  4atex2-0cOLDN  40063  cdleme0moN  40208  cdleme16e  40265  cdleme17d1  40272  cdleme18d  40278  cdleme19d  40289  cdleme20f  40297  cdleme20g  40298  cdleme21ct  40312  cdleme22aa  40322  cdleme22cN  40325  cdleme22d  40326  cdleme22e  40327  cdleme22eALTN  40328  cdleme26e  40342  cdleme32e  40428  cdleme32f  40429  cdlemg4  40600  cdlemg18d  40664  cdlemg18  40665  cdlemg19a  40666  cdlemg19  40667  cdlemg21  40669  cdlemg33b0  40684  cdlemk5  40819  cdlemk6  40820  cdlemk7  40831  cdlemk11  40832  cdlemk12  40833  cdlemk21N  40856  cdlemk20  40857  cdlemk28-3  40891  cdlemk34  40893  cdlemkfid3N  40908  cdlemk55u1  40948