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  38367  paddasslem15  38410  4atex2-0aOLDN  38654  4atex3  38657  trlval3  38763  cdleme12  38847  cdleme19b  38880  cdleme19d  38882  cdleme19e  38883  cdleme20d  38888  cdleme20f  38890  cdleme20g  38891  cdleme21d  38906  cdleme21e  38907  cdleme21f  38908  cdleme22cN  38918  cdleme22e  38920  cdleme22f2  38923  cdleme22g  38924  cdleme26e  38935  cdleme28a  38946  cdleme37m  39038  cdleme39n  39042  cdlemg28b  39279  cdlemk3  39409  cdlemk12  39426  cdlemk12u  39448  cdlemkoatnle-2N  39451  cdlemk13-2N  39452  cdlemkole-2N  39453  cdlemk14-2N  39454  cdlemk15-2N  39455  cdlemk16-2N  39456  cdlemk17-2N  39457  cdlemk18-2N  39462  cdlemk19-2N  39463  cdlemk7u-2N  39464  cdlemk11u-2N  39465  cdlemk20-2N  39468  cdlemk30  39470  cdlemk23-3  39478  cdlemk24-3  39479