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  14209  segconeu  35994  4atlem10  39595  lplncvrlvol2  39604  4atex  40065  4atex2-0cOLDN  40069  cdleme0moN  40214  cdleme16e  40271  cdleme17d1  40278  cdleme18d  40284  cdleme19d  40295  cdleme20f  40303  cdleme20g  40304  cdleme21ct  40318  cdleme22aa  40328  cdleme22cN  40331  cdleme22d  40332  cdleme22e  40333  cdleme22eALTN  40334  cdleme26e  40348  cdleme32e  40434  cdleme32f  40435  cdlemg4  40606  cdlemg18d  40670  cdlemg18  40671  cdlemg19a  40672  cdlemg19  40673  cdlemg21  40675  cdlemg33b0  40690  cdlemk5  40825  cdlemk6  40826  cdlemk7  40837  cdlemk11  40838  cdlemk12  40839  cdlemk21N  40862  cdlemk20  40863  cdlemk28-3  40897  cdlemk34  40899  cdlemkfid3N  40914  cdlemk55u1  40954