Theorem simp21r 1172

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

Assertion

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

Proof of Theorem simp21r

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  modexp  12861  segconeu  31288  4atlem10  33910  lplncvrlvol2  33919  4atex  34380  4atex2-0cOLDN  34384  cdleme0moN  34530  cdleme16e  34587  cdleme17d1  34594  cdleme18d  34600  cdleme19d  34612  cdleme20f  34620  cdleme20g  34621  cdleme21ct  34635  cdleme22aa  34645  cdleme22cN  34648  cdleme22d  34649  cdleme22e  34650  cdleme22eALTN  34651  cdleme26e  34665  cdleme32e  34751  cdleme32f  34752  cdlemg4  34923  cdlemg18d  34987  cdlemg18  34988  cdlemg19a  34989  cdlemg19  34990  cdlemg21  34992  cdlemg33b0  35007  cdlemk5  35142  cdlemk6  35143  cdlemk7  35154  cdlemk11  35155  cdlemk12  35156  cdlemk21N  35179  cdlemk20  35180  cdlemk28-3  35214  cdlemk34  35216  cdlemkfid3N  35231  cdlemk55u1  35271