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 397   ∧ 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 206  df-an 398  df-3an 1090

This theorem is referenced by:  cdlema1N  38710  paddasslem15  38753  4atex2-0aOLDN  38997  4atex3  39000  trlval3  39106  cdleme12  39190  cdleme19b  39223  cdleme19d  39225  cdleme19e  39226  cdleme20d  39231  cdleme20f  39233  cdleme20g  39234  cdleme21d  39249  cdleme21e  39250  cdleme21f  39251  cdleme22cN  39261  cdleme22e  39263  cdleme22f2  39266  cdleme22g  39267  cdleme26e  39278  cdleme28a  39289  cdleme37m  39381  cdleme39n  39385  cdlemg28b  39622  cdlemk3  39752  cdlemk12  39769  cdlemk12u  39791  cdlemkoatnle-2N  39794  cdlemk13-2N  39795  cdlemkole-2N  39796  cdlemk14-2N  39797  cdlemk15-2N  39798  cdlemk16-2N  39799  cdlemk17-2N  39800  cdlemk18-2N  39805  cdlemk19-2N  39806  cdlemk7u-2N  39807  cdlemk11u-2N  39808  cdlemk20-2N  39811  cdlemk30  39813  cdlemk23-3  39821  cdlemk24-3  39822