Theorem simp21r 1304

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

Assertion

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

Proof of Theorem simp21r

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  modexp  14248  segconeu  36325  4atlem10  40194  lplncvrlvol2  40203  4atex  40664  4atex2-0cOLDN  40668  cdleme0moN  40813  cdleme16e  40870  cdleme17d1  40877  cdleme18d  40883  cdleme19d  40894  cdleme20f  40902  cdleme20g  40903  cdleme21ct  40917  cdleme22aa  40927  cdleme22cN  40930  cdleme22d  40931  cdleme22e  40932  cdleme22eALTN  40933  cdleme26e  40947  cdleme32e  41033  cdleme32f  41034  cdlemg4  41205  cdlemg18d  41269  cdlemg18  41270  cdlemg19a  41271  cdlemg19  41272  cdlemg21  41274  cdlemg33b0  41289  cdlemk5  41424  cdlemk6  41425  cdlemk7  41436  cdlemk11  41437  cdlemk12  41438  cdlemk21N  41461  cdlemk20  41462  cdlemk28-3  41496  cdlemk34  41498  cdlemkfid3N  41513  cdlemk55u1  41553