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  14200  segconeu  36193  4atlem10  40052  lplncvrlvol2  40061  4atex  40522  4atex2-0cOLDN  40526  cdleme0moN  40671  cdleme16e  40728  cdleme17d1  40735  cdleme18d  40741  cdleme19d  40752  cdleme20f  40760  cdleme20g  40761  cdleme21ct  40775  cdleme22aa  40785  cdleme22cN  40788  cdleme22d  40789  cdleme22e  40790  cdleme22eALTN  40791  cdleme26e  40805  cdleme32e  40891  cdleme32f  40892  cdlemg4  41063  cdlemg18d  41127  cdlemg18  41128  cdlemg19a  41129  cdlemg19  41130  cdlemg21  41132  cdlemg33b0  41147  cdlemk5  41282  cdlemk6  41283  cdlemk7  41294  cdlemk11  41295  cdlemk12  41296  cdlemk21N  41319  cdlemk20  41320  cdlemk28-3  41354  cdlemk34  41356  cdlemkfid3N  41371  cdlemk55u1  41411