Theorem simp21r 1347

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

Assertion

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

Proof of Theorem simp21r

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  modexp  13318  segconeu  32707  4atlem10  35760  lplncvrlvol2  35769  4atex  36230  4atex2-0cOLDN  36234  cdleme0moN  36379  cdleme16e  36436  cdleme17d1  36443  cdleme18d  36449  cdleme19d  36460  cdleme20f  36468  cdleme20g  36469  cdleme21ct  36483  cdleme22aa  36493  cdleme22cN  36496  cdleme22d  36497  cdleme22e  36498  cdleme22eALTN  36499  cdleme26e  36513  cdleme32e  36599  cdleme32f  36600  cdlemg4  36771  cdlemg18d  36835  cdlemg18  36836  cdlemg19a  36837  cdlemg19  36838  cdlemg21  36840  cdlemg33b0  36855  cdlemk5  36990  cdlemk6  36991  cdlemk7  37002  cdlemk11  37003  cdlemk12  37004  cdlemk21N  37027  cdlemk20  37028  cdlemk28-3  37062  cdlemk34  37064  cdlemkfid3N  37079  cdlemk55u1  37119