Theorem simp21r 1291

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

Assertion

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

Proof of Theorem simp21r

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  modexp  14197  segconeu  34971  4atlem10  38465  lplncvrlvol2  38474  4atex  38935  4atex2-0cOLDN  38939  cdleme0moN  39084  cdleme16e  39141  cdleme17d1  39148  cdleme18d  39154  cdleme19d  39165  cdleme20f  39173  cdleme20g  39174  cdleme21ct  39188  cdleme22aa  39198  cdleme22cN  39201  cdleme22d  39202  cdleme22e  39203  cdleme22eALTN  39204  cdleme26e  39218  cdleme32e  39304  cdleme32f  39305  cdlemg4  39476  cdlemg18d  39540  cdlemg18  39541  cdlemg19a  39542  cdlemg19  39543  cdlemg21  39545  cdlemg33b0  39560  cdlemk5  39695  cdlemk6  39696  cdlemk7  39707  cdlemk11  39708  cdlemk12  39709  cdlemk21N  39732  cdlemk20  39733  cdlemk28-3  39767  cdlemk34  39769  cdlemkfid3N  39784  cdlemk55u1  39824