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  14256  segconeu  36029  4atlem10  39625  lplncvrlvol2  39634  4atex  40095  4atex2-0cOLDN  40099  cdleme0moN  40244  cdleme16e  40301  cdleme17d1  40308  cdleme18d  40314  cdleme19d  40325  cdleme20f  40333  cdleme20g  40334  cdleme21ct  40348  cdleme22aa  40358  cdleme22cN  40361  cdleme22d  40362  cdleme22e  40363  cdleme22eALTN  40364  cdleme26e  40378  cdleme32e  40464  cdleme32f  40465  cdlemg4  40636  cdlemg18d  40700  cdlemg18  40701  cdlemg19a  40702  cdlemg19  40703  cdlemg21  40705  cdlemg33b0  40720  cdlemk5  40855  cdlemk6  40856  cdlemk7  40867  cdlemk11  40868  cdlemk12  40869  cdlemk21N  40892  cdlemk20  40893  cdlemk28-3  40927  cdlemk34  40929  cdlemkfid3N  40944  cdlemk55u1  40984