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  40051  paddasslem15  40094  4atex2-0aOLDN  40338  4atex3  40341  cdleme19b  40564  cdleme19d  40566  cdleme19e  40567  cdleme20d  40572  cdleme20f  40574  cdleme20g  40575  cdleme21d  40590  cdleme21e  40591  cdleme22cN  40602  cdleme22e  40604  cdleme22f2  40607  cdleme26e  40619  cdleme28a  40630  cdleme37m  40722  cdlemg28b  40963  cdlemk3  41093  cdlemk12  41110  cdlemk12u  41132  cdlemkoatnle-2N  41135  cdlemk13-2N  41136  cdlemkole-2N  41137  cdlemk14-2N  41138  cdlemk15-2N  41139  cdlemk16-2N  41140  cdlemk17-2N  41141  cdlemk18-2N  41146  cdlemk19-2N  41147  cdlemk7u-2N  41148  cdlemk11u-2N  41149  cdlemk20-2N  41152  cdlemk30  41154  cdlemk23-3  41162  cdlemk24-3  41163