Theorem simp21r 1298

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

Assertion

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

Proof of Theorem simp21r

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  modexp  14198  segconeu  36246  4atlem10  40105  lplncvrlvol2  40114  4atex  40575  4atex2-0cOLDN  40579  cdleme0moN  40724  cdleme16e  40781  cdleme17d1  40788  cdleme18d  40794  cdleme19d  40805  cdleme20f  40813  cdleme20g  40814  cdleme21ct  40828  cdleme22aa  40838  cdleme22cN  40841  cdleme22d  40842  cdleme22e  40843  cdleme22eALTN  40844  cdleme26e  40858  cdleme32e  40944  cdleme32f  40945  cdlemg4  41116  cdlemg18d  41180  cdlemg18  41181  cdlemg19a  41182  cdlemg19  41183  cdlemg21  41185  cdlemg33b0  41200  cdlemk5  41335  cdlemk6  41336  cdlemk7  41347  cdlemk11  41348  cdlemk12  41349  cdlemk21N  41372  cdlemk20  41373  cdlemk28-3  41407  cdlemk34  41409  cdlemkfid3N  41424  cdlemk55u1  41464