Theorem simp32r 1297

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

Assertion

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

Proof of Theorem simp32r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  cdlema1N  37732  paddasslem15  37775  4atex2-0aOLDN  38019  4atex3  38022  cdleme19b  38245  cdleme19d  38247  cdleme19e  38248  cdleme20d  38253  cdleme20f  38255  cdleme20g  38256  cdleme21d  38271  cdleme21e  38272  cdleme22cN  38283  cdleme22e  38285  cdleme22f2  38288  cdleme26e  38300  cdleme28a  38311  cdleme37m  38403  cdlemg28b  38644  cdlemk3  38774  cdlemk12  38791  cdlemk12u  38813  cdlemkoatnle-2N  38816  cdlemk13-2N  38817  cdlemkole-2N  38818  cdlemk14-2N  38819  cdlemk15-2N  38820  cdlemk16-2N  38821  cdlemk17-2N  38822  cdlemk18-2N  38827  cdlemk19-2N  38828  cdlemk7u-2N  38829  cdlemk11u-2N  38830  cdlemk20-2N  38833  cdlemk30  38835  cdlemk23-3  38843  cdlemk24-3  38844