Theorem simp32l 1299

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

Assertion

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

Proof of Theorem simp32l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088

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 210  df-an 400  df-3an 1090

This theorem is referenced by:  cdlema1N  37417  paddasslem15  37460  4atex2-0aOLDN  37704  4atex3  37707  trlval3  37813  cdleme12  37897  cdleme19b  37930  cdleme19d  37932  cdleme19e  37933  cdleme20d  37938  cdleme20f  37940  cdleme20g  37941  cdleme21d  37956  cdleme21e  37957  cdleme21f  37958  cdleme22cN  37968  cdleme22e  37970  cdleme22f2  37973  cdleme22g  37974  cdleme26e  37985  cdleme28a  37996  cdleme37m  38088  cdleme39n  38092  cdlemg28b  38329  cdlemk3  38459  cdlemk12  38476  cdlemk12u  38498  cdlemkoatnle-2N  38501  cdlemk13-2N  38502  cdlemkole-2N  38503  cdlemk14-2N  38504  cdlemk15-2N  38505  cdlemk16-2N  38506  cdlemk17-2N  38507  cdlemk18-2N  38512  cdlemk19-2N  38513  cdlemk7u-2N  38514  cdlemk11u-2N  38515  cdlemk20-2N  38518  cdlemk30  38520  cdlemk23-3  38528  cdlemk24-3  38529