Theorem simp32l 1294

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

Assertion

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

Proof of Theorem simp32l

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  cdlema1N  36929  paddasslem15  36972  4atex2-0aOLDN  37216  4atex3  37219  trlval3  37325  cdleme12  37409  cdleme19b  37442  cdleme19d  37444  cdleme19e  37445  cdleme20d  37450  cdleme20f  37452  cdleme20g  37453  cdleme21d  37468  cdleme21e  37469  cdleme21f  37470  cdleme22cN  37480  cdleme22e  37482  cdleme22f2  37485  cdleme22g  37486  cdleme26e  37497  cdleme28a  37508  cdleme37m  37600  cdleme39n  37604  cdlemg28b  37841  cdlemk3  37971  cdlemk12  37988  cdlemk12u  38010  cdlemkoatnle-2N  38013  cdlemk13-2N  38014  cdlemkole-2N  38015  cdlemk14-2N  38016  cdlemk15-2N  38017  cdlemk16-2N  38018  cdlemk17-2N  38019  cdlemk18-2N  38024  cdlemk19-2N  38025  cdlemk7u-2N  38026  cdlemk11u-2N  38027  cdlemk20-2N  38030  cdlemk30  38032  cdlemk23-3  38040  cdlemk24-3  38041