Theorem simp32r 1296

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

Assertion

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

Proof of Theorem simp32r

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  cdlema1N  39296  paddasslem15  39339  4atex2-0aOLDN  39583  4atex3  39586  cdleme19b  39809  cdleme19d  39811  cdleme19e  39812  cdleme20d  39817  cdleme20f  39819  cdleme20g  39820  cdleme21d  39835  cdleme21e  39836  cdleme22cN  39847  cdleme22e  39849  cdleme22f2  39852  cdleme26e  39864  cdleme28a  39875  cdleme37m  39967  cdlemg28b  40208  cdlemk3  40338  cdlemk12  40355  cdlemk12u  40377  cdlemkoatnle-2N  40380  cdlemk13-2N  40381  cdlemkole-2N  40382  cdlemk14-2N  40383  cdlemk15-2N  40384  cdlemk16-2N  40385  cdlemk17-2N  40386  cdlemk18-2N  40391  cdlemk19-2N  40392  cdlemk7u-2N  40393  cdlemk11u-2N  40394  cdlemk20-2N  40397  cdlemk30  40399  cdlemk23-3  40407  cdlemk24-3  40408