Theorem simp21r 1383

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

Assertion

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

Proof of Theorem simp21r

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  modexp  13218  segconeu  32436  4atlem10  35383  lplncvrlvol2  35392  4atex  35853  4atex2-0cOLDN  35857  cdleme0moN  36003  cdleme16e  36060  cdleme17d1  36067  cdleme18d  36073  cdleme19d  36084  cdleme20f  36092  cdleme20g  36093  cdleme21ct  36107  cdleme22aa  36117  cdleme22cN  36120  cdleme22d  36121  cdleme22e  36122  cdleme22eALTN  36123  cdleme26e  36137  cdleme32e  36223  cdleme32f  36224  cdlemg4  36395  cdlemg18d  36459  cdlemg18  36460  cdlemg19a  36461  cdlemg19  36462  cdlemg21  36464  cdlemg33b0  36479  cdlemk5  36614  cdlemk6  36615  cdlemk7  36626  cdlemk11  36627  cdlemk12  36628  cdlemk21N  36651  cdlemk20  36652  cdlemk28-3  36686  cdlemk34  36688  cdlemkfid3N  36703  cdlemk55u1  36743