Theorem simp21r 1288

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

Assertion

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

Proof of Theorem simp21r

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

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

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 1086

This theorem is referenced by:  modexp  13595  segconeu  33585  4atlem10  36902  lplncvrlvol2  36911  4atex  37372  4atex2-0cOLDN  37376  cdleme0moN  37521  cdleme16e  37578  cdleme17d1  37585  cdleme18d  37591  cdleme19d  37602  cdleme20f  37610  cdleme20g  37611  cdleme21ct  37625  cdleme22aa  37635  cdleme22cN  37638  cdleme22d  37639  cdleme22e  37640  cdleme22eALTN  37641  cdleme26e  37655  cdleme32e  37741  cdleme32f  37742  cdlemg4  37913  cdlemg18d  37977  cdlemg18  37978  cdlemg19a  37979  cdlemg19  37980  cdlemg21  37982  cdlemg33b0  37997  cdlemk5  38132  cdlemk6  38133  cdlemk7  38144  cdlemk11  38145  cdlemk12  38146  cdlemk21N  38169  cdlemk20  38170  cdlemk28-3  38204  cdlemk34  38206  cdlemkfid3N  38221  cdlemk55u1  38261