Theorem simp21r 1291

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

Assertion

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

Proof of Theorem simp21r

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

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

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 1089

This theorem is referenced by:  modexp  14287  segconeu  35975  4atlem10  39563  lplncvrlvol2  39572  4atex  40033  4atex2-0cOLDN  40037  cdleme0moN  40182  cdleme16e  40239  cdleme17d1  40246  cdleme18d  40252  cdleme19d  40263  cdleme20f  40271  cdleme20g  40272  cdleme21ct  40286  cdleme22aa  40296  cdleme22cN  40299  cdleme22d  40300  cdleme22e  40301  cdleme22eALTN  40302  cdleme26e  40316  cdleme32e  40402  cdleme32f  40403  cdlemg4  40574  cdlemg18d  40638  cdlemg18  40639  cdlemg19a  40640  cdlemg19  40641  cdlemg21  40643  cdlemg33b0  40658  cdlemk5  40793  cdlemk6  40794  cdlemk7  40805  cdlemk11  40806  cdlemk12  40807  cdlemk21N  40830  cdlemk20  40831  cdlemk28-3  40865  cdlemk34  40867  cdlemkfid3N  40882  cdlemk55u1  40922