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  14210  segconeu  36006  4atlem10  39607  lplncvrlvol2  39616  4atex  40077  4atex2-0cOLDN  40081  cdleme0moN  40226  cdleme16e  40283  cdleme17d1  40290  cdleme18d  40296  cdleme19d  40307  cdleme20f  40315  cdleme20g  40316  cdleme21ct  40330  cdleme22aa  40340  cdleme22cN  40343  cdleme22d  40344  cdleme22e  40345  cdleme22eALTN  40346  cdleme26e  40360  cdleme32e  40446  cdleme32f  40447  cdlemg4  40618  cdlemg18d  40682  cdlemg18  40683  cdlemg19a  40684  cdlemg19  40685  cdlemg21  40687  cdlemg33b0  40702  cdlemk5  40837  cdlemk6  40838  cdlemk7  40849  cdlemk11  40850  cdlemk12  40851  cdlemk21N  40874  cdlemk20  40875  cdlemk28-3  40909  cdlemk34  40911  cdlemkfid3N  40926  cdlemk55u1  40966