Theorem simp32r 1318

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

Assertion

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

Proof of Theorem simp32r

Step	Hyp	Ref	Expression
1		simp2r 1219	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant3 1153	1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  cdlema1N  40664  paddasslem15  40707  4atex2-0aOLDN  40951  4atex3  40954  cdleme19b  41177  cdleme19d  41179  cdleme19e  41180  cdleme20d  41185  cdleme20f  41187  cdleme20g  41188  cdleme21d  41203  cdleme21e  41204  cdleme22cN  41215  cdleme22e  41217  cdleme22f2  41220  cdleme26e  41232  cdleme28a  41243  cdleme37m  41335  cdlemg28b  41576  cdlemk3  41706  cdlemk12  41723  cdlemk12u  41745  cdlemkoatnle-2N  41748  cdlemk13-2N  41749  cdlemkole-2N  41750  cdlemk14-2N  41751  cdlemk15-2N  41752  cdlemk16-2N  41753  cdlemk17-2N  41754  cdlemk18-2N  41759  cdlemk19-2N  41760  cdlemk7u-2N  41761  cdlemk11u-2N  41762  cdlemk20-2N  41765  cdlemk30  41767  cdlemk23-3  41775  cdlemk24-3  41776