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 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  14277  segconeu  36012  4atlem10  39608  lplncvrlvol2  39617  4atex  40078  4atex2-0cOLDN  40082  cdleme0moN  40227  cdleme16e  40284  cdleme17d1  40291  cdleme18d  40297  cdleme19d  40308  cdleme20f  40316  cdleme20g  40317  cdleme21ct  40331  cdleme22aa  40341  cdleme22cN  40344  cdleme22d  40345  cdleme22e  40346  cdleme22eALTN  40347  cdleme26e  40361  cdleme32e  40447  cdleme32f  40448  cdlemg4  40619  cdlemg18d  40683  cdlemg18  40684  cdlemg19a  40685  cdlemg19  40686  cdlemg21  40688  cdlemg33b0  40703  cdlemk5  40838  cdlemk6  40839  cdlemk7  40850  cdlemk11  40851  cdlemk12  40852  cdlemk21N  40875  cdlemk20  40876  cdlemk28-3  40910  cdlemk34  40912  cdlemkfid3N  40927  cdlemk55u1  40967