Theorem simp21r 1292

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

Assertion

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

Proof of Theorem simp21r

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

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

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 1088

This theorem is referenced by:  modexp  14145  segconeu  36051  4atlem10  39651  lplncvrlvol2  39660  4atex  40121  4atex2-0cOLDN  40125  cdleme0moN  40270  cdleme16e  40327  cdleme17d1  40334  cdleme18d  40340  cdleme19d  40351  cdleme20f  40359  cdleme20g  40360  cdleme21ct  40374  cdleme22aa  40384  cdleme22cN  40387  cdleme22d  40388  cdleme22e  40389  cdleme22eALTN  40390  cdleme26e  40404  cdleme32e  40490  cdleme32f  40491  cdlemg4  40662  cdlemg18d  40726  cdlemg18  40727  cdlemg19a  40728  cdlemg19  40729  cdlemg21  40731  cdlemg33b0  40746  cdlemk5  40881  cdlemk6  40882  cdlemk7  40893  cdlemk11  40894  cdlemk12  40895  cdlemk21N  40918  cdlemk20  40919  cdlemk28-3  40953  cdlemk34  40955  cdlemkfid3N  40970  cdlemk55u1  41010