Theorem simp21r 1293

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

Assertion

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

Proof of Theorem simp21r

Step	Hyp	Ref	Expression
1		simp1r 1200	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1135	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  14173  segconeu  36224  4atlem10  39976  lplncvrlvol2  39985  4atex  40446  4atex2-0cOLDN  40450  cdleme0moN  40595  cdleme16e  40652  cdleme17d1  40659  cdleme18d  40665  cdleme19d  40676  cdleme20f  40684  cdleme20g  40685  cdleme21ct  40699  cdleme22aa  40709  cdleme22cN  40712  cdleme22d  40713  cdleme22e  40714  cdleme22eALTN  40715  cdleme26e  40729  cdleme32e  40815  cdleme32f  40816  cdlemg4  40987  cdlemg18d  41051  cdlemg18  41052  cdlemg19a  41053  cdlemg19  41054  cdlemg21  41056  cdlemg33b0  41071  cdlemk5  41206  cdlemk6  41207  cdlemk7  41218  cdlemk11  41219  cdlemk12  41220  cdlemk21N  41243  cdlemk20  41244  cdlemk28-3  41278  cdlemk34  41280  cdlemkfid3N  41295  cdlemk55u1  41335