Theorem simp21r 1310

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

Assertion

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

Proof of Theorem simp21r

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  modexp  14276  segconeu  36481  4atlem10  40358  lplncvrlvol2  40367  4atex  40828  4atex2-0cOLDN  40832  cdleme0moN  40977  cdleme16e  41034  cdleme17d1  41041  cdleme18d  41047  cdleme19d  41058  cdleme20f  41066  cdleme20g  41067  cdleme21ct  41081  cdleme22aa  41091  cdleme22cN  41094  cdleme22d  41095  cdleme22e  41096  cdleme22eALTN  41097  cdleme26e  41111  cdleme32e  41197  cdleme32f  41198  cdlemg4  41369  cdlemg18d  41433  cdlemg18  41434  cdlemg19a  41435  cdlemg19  41436  cdlemg21  41438  cdlemg33b0  41453  cdlemk5  41588  cdlemk6  41589  cdlemk7  41600  cdlemk11  41601  cdlemk12  41602  cdlemk21N  41625  cdlemk20  41626  cdlemk28-3  41660  cdlemk34  41662  cdlemkfid3N  41677  cdlemk55u1  41717