Theorem simp32r 1300

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

Assertion

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

Proof of Theorem simp32r

Step	Hyp	Ref	Expression
1		simp2r 1201	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant3 1135	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:  cdlema1N  39836  paddasslem15  39879  4atex2-0aOLDN  40123  4atex3  40126  cdleme19b  40349  cdleme19d  40351  cdleme19e  40352  cdleme20d  40357  cdleme20f  40359  cdleme20g  40360  cdleme21d  40375  cdleme21e  40376  cdleme22cN  40387  cdleme22e  40389  cdleme22f2  40392  cdleme26e  40404  cdleme28a  40415  cdleme37m  40507  cdlemg28b  40748  cdlemk3  40878  cdlemk12  40895  cdlemk12u  40917  cdlemkoatnle-2N  40920  cdlemk13-2N  40921  cdlemkole-2N  40922  cdlemk14-2N  40923  cdlemk15-2N  40924  cdlemk16-2N  40925  cdlemk17-2N  40926  cdlemk18-2N  40931  cdlemk19-2N  40932  cdlemk7u-2N  40933  cdlemk11u-2N  40934  cdlemk20-2N  40937  cdlemk30  40939  cdlemk23-3  40947  cdlemk24-3  40948