Theorem simp21r 1288

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

Assertion

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

Proof of Theorem simp21r

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  modexp  14255  segconeu  35835  4atlem10  39305  lplncvrlvol2  39314  4atex  39775  4atex2-0cOLDN  39779  cdleme0moN  39924  cdleme16e  39981  cdleme17d1  39988  cdleme18d  39994  cdleme19d  40005  cdleme20f  40013  cdleme20g  40014  cdleme21ct  40028  cdleme22aa  40038  cdleme22cN  40041  cdleme22d  40042  cdleme22e  40043  cdleme22eALTN  40044  cdleme26e  40058  cdleme32e  40144  cdleme32f  40145  cdlemg4  40316  cdlemg18d  40380  cdlemg18  40381  cdlemg19a  40382  cdlemg19  40383  cdlemg21  40385  cdlemg33b0  40400  cdlemk5  40535  cdlemk6  40536  cdlemk7  40547  cdlemk11  40548  cdlemk12  40549  cdlemk21N  40572  cdlemk20  40573  cdlemk28-3  40607  cdlemk34  40609  cdlemkfid3N  40624  cdlemk55u1  40664