Theorem simp32l 1300

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

Assertion

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

Proof of Theorem simp32l

Step	Hyp	Ref	Expression
1		simp2l 1201	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜑)
2	1	3ad2ant3 1136	1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑)

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

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 1089

This theorem is referenced by:  cdlema1N  40251  paddasslem15  40294  4atex2-0aOLDN  40538  4atex3  40541  trlval3  40647  cdleme12  40731  cdleme19b  40764  cdleme19d  40766  cdleme19e  40767  cdleme20d  40772  cdleme20f  40774  cdleme20g  40775  cdleme21d  40790  cdleme21e  40791  cdleme21f  40792  cdleme22cN  40802  cdleme22e  40804  cdleme22f2  40807  cdleme22g  40808  cdleme26e  40819  cdleme28a  40830  cdleme37m  40922  cdleme39n  40926  cdlemg28b  41163  cdlemk3  41293  cdlemk12  41310  cdlemk12u  41332  cdlemkoatnle-2N  41335  cdlemk13-2N  41336  cdlemkole-2N  41337  cdlemk14-2N  41338  cdlemk15-2N  41339  cdlemk16-2N  41340  cdlemk17-2N  41341  cdlemk18-2N  41346  cdlemk19-2N  41347  cdlemk7u-2N  41348  cdlemk11u-2N  41349  cdlemk20-2N  41352  cdlemk30  41354  cdlemk23-3  41362  cdlemk24-3  41363