Theorem simp21r 1287

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

Assertion

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

Proof of Theorem simp21r

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  modexp  13600  segconeu  33472  4atlem10  36757  lplncvrlvol2  36766  4atex  37227  4atex2-0cOLDN  37231  cdleme0moN  37376  cdleme16e  37433  cdleme17d1  37440  cdleme18d  37446  cdleme19d  37457  cdleme20f  37465  cdleme20g  37466  cdleme21ct  37480  cdleme22aa  37490  cdleme22cN  37493  cdleme22d  37494  cdleme22e  37495  cdleme22eALTN  37496  cdleme26e  37510  cdleme32e  37596  cdleme32f  37597  cdlemg4  37768  cdlemg18d  37832  cdlemg18  37833  cdlemg19a  37834  cdlemg19  37835  cdlemg21  37837  cdlemg33b0  37852  cdlemk5  37987  cdlemk6  37988  cdlemk7  37999  cdlemk11  38000  cdlemk12  38001  cdlemk21N  38024  cdlemk20  38025  cdlemk28-3  38059  cdlemk34  38061  cdlemkfid3N  38076  cdlemk55u1  38116