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  40828  paddasslem15  40871  4atex2-0aOLDN  41115  4atex3  41118  cdleme19b  41341  cdleme19d  41343  cdleme19e  41344  cdleme20d  41349  cdleme20f  41351  cdleme20g  41352  cdleme21d  41367  cdleme21e  41368  cdleme22cN  41379  cdleme22e  41381  cdleme22f2  41384  cdleme26e  41396  cdleme28a  41407  cdleme37m  41499  cdlemg28b  41740  cdlemk3  41870  cdlemk12  41887  cdlemk12u  41909  cdlemkoatnle-2N  41912  cdlemk13-2N  41913  cdlemkole-2N  41914  cdlemk14-2N  41915  cdlemk15-2N  41916  cdlemk16-2N  41917  cdlemk17-2N  41918  cdlemk18-2N  41923  cdlemk19-2N  41924  cdlemk7u-2N  41925  cdlemk11u-2N  41926  cdlemk20-2N  41929  cdlemk30  41931  cdlemk23-3  41939  cdlemk24-3  41940