Theorem simp21r 1293

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

Assertion

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

Proof of Theorem simp21r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  modexp  14191  segconeu  36209  4atlem10  40066  lplncvrlvol2  40075  4atex  40536  4atex2-0cOLDN  40540  cdleme0moN  40685  cdleme16e  40742  cdleme17d1  40749  cdleme18d  40755  cdleme19d  40766  cdleme20f  40774  cdleme20g  40775  cdleme21ct  40789  cdleme22aa  40799  cdleme22cN  40802  cdleme22d  40803  cdleme22e  40804  cdleme22eALTN  40805  cdleme26e  40819  cdleme32e  40905  cdleme32f  40906  cdlemg4  41077  cdlemg18d  41141  cdlemg18  41142  cdlemg19a  41143  cdlemg19  41144  cdlemg21  41146  cdlemg33b0  41161  cdlemk5  41296  cdlemk6  41297  cdlemk7  41308  cdlemk11  41309  cdlemk12  41310  cdlemk21N  41333  cdlemk20  41334  cdlemk28-3  41368  cdlemk34  41370  cdlemkfid3N  41385  cdlemk55u1  41425