Theorem simp21r 1374

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

Assertion

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

Proof of Theorem simp21r

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1070

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 197  df-an 383  df-3an 1072

This theorem is referenced by:  modexp  13205  segconeu  32449  4atlem10  35407  lplncvrlvol2  35416  4atex  35877  4atex2-0cOLDN  35881  cdleme0moN  36027  cdleme16e  36084  cdleme17d1  36091  cdleme18d  36097  cdleme19d  36108  cdleme20f  36116  cdleme20g  36117  cdleme21ct  36131  cdleme22aa  36141  cdleme22cN  36144  cdleme22d  36145  cdleme22e  36146  cdleme22eALTN  36147  cdleme26e  36161  cdleme32e  36247  cdleme32f  36248  cdlemg4  36419  cdlemg18d  36483  cdlemg18  36484  cdlemg19a  36485  cdlemg19  36486  cdlemg21  36488  cdlemg33b0  36503  cdlemk5  36638  cdlemk6  36639  cdlemk7  36650  cdlemk11  36651  cdlemk12  36652  cdlemk21N  36675  cdlemk20  36676  cdlemk28-3  36710  cdlemk34  36712  cdlemkfid3N  36727  cdlemk55u1  36767