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  41114  paddasslem15  41157  4atex2-0aOLDN  41401  4atex3  41404  cdleme19b  41627  cdleme19d  41629  cdleme19e  41630  cdleme20d  41635  cdleme20f  41637  cdleme20g  41638  cdleme21d  41653  cdleme21e  41654  cdleme22cN  41665  cdleme22e  41667  cdleme22f2  41670  cdleme26e  41682  cdleme28a  41693  cdleme37m  41785  cdlemg28b  42026  cdlemk3  42156  cdlemk12  42173  cdlemk12u  42195  cdlemkoatnle-2N  42198  cdlemk13-2N  42199  cdlemkole-2N  42200  cdlemk14-2N  42201  cdlemk15-2N  42202  cdlemk16-2N  42203  cdlemk17-2N  42204  cdlemk18-2N  42209  cdlemk19-2N  42210  cdlemk7u-2N  42211  cdlemk11u-2N  42212  cdlemk20-2N  42215  cdlemk30  42217  cdlemk23-3  42225  cdlemk24-3  42226