Theorem simp21r 1292

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

Assertion

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

Proof of Theorem simp21r

Step	Hyp	Ref	Expression
1		simp1r 1199	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1134	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  14161  segconeu  36205  4atlem10  39862  lplncvrlvol2  39871  4atex  40332  4atex2-0cOLDN  40336  cdleme0moN  40481  cdleme16e  40538  cdleme17d1  40545  cdleme18d  40551  cdleme19d  40562  cdleme20f  40570  cdleme20g  40571  cdleme21ct  40585  cdleme22aa  40595  cdleme22cN  40598  cdleme22d  40599  cdleme22e  40600  cdleme22eALTN  40601  cdleme26e  40615  cdleme32e  40701  cdleme32f  40702  cdlemg4  40873  cdlemg18d  40937  cdlemg18  40938  cdlemg19a  40939  cdlemg19  40940  cdlemg21  40942  cdlemg33b0  40957  cdlemk5  41092  cdlemk6  41093  cdlemk7  41104  cdlemk11  41105  cdlemk12  41106  cdlemk21N  41129  cdlemk20  41130  cdlemk28-3  41164  cdlemk34  41166  cdlemkfid3N  41181  cdlemk55u1  41221