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  40955  paddasslem15  40998  4atex2-0aOLDN  41242  4atex3  41245  cdleme19b  41468  cdleme19d  41470  cdleme19e  41471  cdleme20d  41476  cdleme20f  41478  cdleme20g  41479  cdleme21d  41494  cdleme21e  41495  cdleme22cN  41506  cdleme22e  41508  cdleme22f2  41511  cdleme26e  41523  cdleme28a  41534  cdleme37m  41626  cdlemg28b  41867  cdlemk3  41997  cdlemk12  42014  cdlemk12u  42036  cdlemkoatnle-2N  42039  cdlemk13-2N  42040  cdlemkole-2N  42041  cdlemk14-2N  42042  cdlemk15-2N  42043  cdlemk16-2N  42044  cdlemk17-2N  42045  cdlemk18-2N  42050  cdlemk19-2N  42051  cdlemk7u-2N  42052  cdlemk11u-2N  42053  cdlemk20-2N  42056  cdlemk30  42058  cdlemk23-3  42066  cdlemk24-3  42067