Theorem simp32l 1317

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

Assertion

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

Proof of Theorem simp32l

Step	Hyp	Ref	Expression
1		simp2l 1218	. 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  40816  paddasslem15  40859  4atex2-0aOLDN  41103  4atex3  41106  trlval3  41212  cdleme12  41296  cdleme19b  41329  cdleme19d  41331  cdleme19e  41332  cdleme20d  41337  cdleme20f  41339  cdleme20g  41340  cdleme21d  41355  cdleme21e  41356  cdleme21f  41357  cdleme22cN  41367  cdleme22e  41369  cdleme22f2  41372  cdleme22g  41373  cdleme26e  41384  cdleme28a  41395  cdleme37m  41487  cdleme39n  41491  cdlemg28b  41728  cdlemk3  41858  cdlemk12  41875  cdlemk12u  41897  cdlemkoatnle-2N  41900  cdlemk13-2N  41901  cdlemkole-2N  41902  cdlemk14-2N  41903  cdlemk15-2N  41904  cdlemk16-2N  41905  cdlemk17-2N  41906  cdlemk18-2N  41911  cdlemk19-2N  41912  cdlemk7u-2N  41913  cdlemk11u-2N  41914  cdlemk20-2N  41917  cdlemk30  41919  cdlemk23-3  41927  cdlemk24-3  41928