Theorem simp32l 1296

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

Assertion

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

Proof of Theorem simp32l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  cdlema1N  37732  paddasslem15  37775  4atex2-0aOLDN  38019  4atex3  38022  trlval3  38128  cdleme12  38212  cdleme19b  38245  cdleme19d  38247  cdleme19e  38248  cdleme20d  38253  cdleme20f  38255  cdleme20g  38256  cdleme21d  38271  cdleme21e  38272  cdleme21f  38273  cdleme22cN  38283  cdleme22e  38285  cdleme22f2  38288  cdleme22g  38289  cdleme26e  38300  cdleme28a  38311  cdleme37m  38403  cdleme39n  38407  cdlemg28b  38644  cdlemk3  38774  cdlemk12  38791  cdlemk12u  38813  cdlemkoatnle-2N  38816  cdlemk13-2N  38817  cdlemkole-2N  38818  cdlemk14-2N  38819  cdlemk15-2N  38820  cdlemk16-2N  38821  cdlemk17-2N  38822  cdlemk18-2N  38827  cdlemk19-2N  38828  cdlemk7u-2N  38829  cdlemk11u-2N  38830  cdlemk20-2N  38833  cdlemk30  38835  cdlemk23-3  38843  cdlemk24-3  38844