Theorem simp32l 1401

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

Assertion

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

Proof of Theorem simp32l

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1111

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 199  df-an 387  df-3an 1113

This theorem is referenced by:  cdlema1N  35859  paddasslem15  35902  4atex2-0aOLDN  36146  4atex3  36149  trlval3  36255  cdleme12  36339  cdleme19b  36372  cdleme19d  36374  cdleme19e  36375  cdleme20d  36380  cdleme20f  36382  cdleme20g  36383  cdleme21d  36398  cdleme21e  36399  cdleme21f  36400  cdleme22cN  36410  cdleme22e  36412  cdleme22f2  36415  cdleme22g  36416  cdleme26e  36427  cdleme28a  36438  cdleme37m  36530  cdleme39n  36534  cdlemg28b  36771  cdlemk3  36901  cdlemk12  36918  cdlemk12u  36940  cdlemkoatnle-2N  36943  cdlemk13-2N  36944  cdlemkole-2N  36945  cdlemk14-2N  36946  cdlemk15-2N  36947  cdlemk16-2N  36948  cdlemk17-2N  36949  cdlemk18-2N  36954  cdlemk19-2N  36955  cdlemk7u-2N  36956  cdlemk11u-2N  36957  cdlemk20-2N  36960  cdlemk30  36962  cdlemk23-3  36970  cdlemk24-3  36971