Theorem simp32l 1298

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

Assertion

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

Proof of Theorem simp32l

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  cdlema1N  38467  paddasslem15  38510  4atex2-0aOLDN  38754  4atex3  38757  trlval3  38863  cdleme12  38947  cdleme19b  38980  cdleme19d  38982  cdleme19e  38983  cdleme20d  38988  cdleme20f  38990  cdleme20g  38991  cdleme21d  39006  cdleme21e  39007  cdleme21f  39008  cdleme22cN  39018  cdleme22e  39020  cdleme22f2  39023  cdleme22g  39024  cdleme26e  39035  cdleme28a  39046  cdleme37m  39138  cdleme39n  39142  cdlemg28b  39379  cdlemk3  39509  cdlemk12  39526  cdlemk12u  39548  cdlemkoatnle-2N  39551  cdlemk13-2N  39552  cdlemkole-2N  39553  cdlemk14-2N  39554  cdlemk15-2N  39555  cdlemk16-2N  39556  cdlemk17-2N  39557  cdlemk18-2N  39562  cdlemk19-2N  39563  cdlemk7u-2N  39564  cdlemk11u-2N  39565  cdlemk20-2N  39568  cdlemk30  39570  cdlemk23-3  39578  cdlemk24-3  39579