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  41040  paddasslem15  41083  4atex2-0aOLDN  41327  4atex3  41330  trlval3  41436  cdleme12  41520  cdleme19b  41553  cdleme19d  41555  cdleme19e  41556  cdleme20d  41561  cdleme20f  41563  cdleme20g  41564  cdleme21d  41579  cdleme21e  41580  cdleme21f  41581  cdleme22cN  41591  cdleme22e  41593  cdleme22f2  41596  cdleme22g  41597  cdleme26e  41608  cdleme28a  41619  cdleme37m  41711  cdleme39n  41715  cdlemg28b  41952  cdlemk3  42082  cdlemk12  42099  cdlemk12u  42121  cdlemkoatnle-2N  42124  cdlemk13-2N  42125  cdlemkole-2N  42126  cdlemk14-2N  42127  cdlemk15-2N  42128  cdlemk16-2N  42129  cdlemk17-2N  42130  cdlemk18-2N  42135  cdlemk19-2N  42136  cdlemk7u-2N  42137  cdlemk11u-2N  42138  cdlemk20-2N  42141  cdlemk30  42143  cdlemk23-3  42151  cdlemk24-3  42152