Theorem simp21r 1308

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

Assertion

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

Proof of Theorem simp21r

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

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

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 1103

This theorem is referenced by:  modexp  14265  segconeu  36374  4atlem10  40242  lplncvrlvol2  40251  4atex  40712  4atex2-0cOLDN  40716  cdleme0moN  40861  cdleme16e  40918  cdleme17d1  40925  cdleme18d  40931  cdleme19d  40942  cdleme20f  40950  cdleme20g  40951  cdleme21ct  40965  cdleme22aa  40975  cdleme22cN  40978  cdleme22d  40979  cdleme22e  40980  cdleme22eALTN  40981  cdleme26e  40995  cdleme32e  41081  cdleme32f  41082  cdlemg4  41253  cdlemg18d  41317  cdlemg18  41318  cdlemg19a  41319  cdlemg19  41320  cdlemg21  41322  cdlemg33b0  41337  cdlemk5  41472  cdlemk6  41473  cdlemk7  41484  cdlemk11  41485  cdlemk12  41486  cdlemk21N  41509  cdlemk20  41510  cdlemk28-3  41544  cdlemk34  41546  cdlemkfid3N  41561  cdlemk55u1  41601