Theorem simp32l 1317

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

Assertion

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

Proof of Theorem simp32l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  cdlema1N  40606  paddasslem15  40649  4atex2-0aOLDN  40893  4atex3  40896  trlval3  41002  cdleme12  41086  cdleme19b  41119  cdleme19d  41121  cdleme19e  41122  cdleme20d  41127  cdleme20f  41129  cdleme20g  41130  cdleme21d  41145  cdleme21e  41146  cdleme21f  41147  cdleme22cN  41157  cdleme22e  41159  cdleme22f2  41162  cdleme22g  41163  cdleme26e  41174  cdleme28a  41185  cdleme37m  41277  cdleme39n  41281  cdlemg28b  41518  cdlemk3  41648  cdlemk12  41665  cdlemk12u  41687  cdlemkoatnle-2N  41690  cdlemk13-2N  41691  cdlemkole-2N  41692  cdlemk14-2N  41693  cdlemk15-2N  41694  cdlemk16-2N  41695  cdlemk17-2N  41696  cdlemk18-2N  41701  cdlemk19-2N  41702  cdlemk7u-2N  41703  cdlemk11u-2N  41704  cdlemk20-2N  41707  cdlemk30  41709  cdlemk23-3  41717  cdlemk24-3  41718