Theorem simp32l 1300

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

Assertion

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

Proof of Theorem simp32l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  cdlema1N  40161  paddasslem15  40204  4atex2-0aOLDN  40448  4atex3  40451  trlval3  40557  cdleme12  40641  cdleme19b  40674  cdleme19d  40676  cdleme19e  40677  cdleme20d  40682  cdleme20f  40684  cdleme20g  40685  cdleme21d  40700  cdleme21e  40701  cdleme21f  40702  cdleme22cN  40712  cdleme22e  40714  cdleme22f2  40717  cdleme22g  40718  cdleme26e  40729  cdleme28a  40740  cdleme37m  40832  cdleme39n  40836  cdlemg28b  41073  cdlemk3  41203  cdlemk12  41220  cdlemk12u  41242  cdlemkoatnle-2N  41245  cdlemk13-2N  41246  cdlemkole-2N  41247  cdlemk14-2N  41248  cdlemk15-2N  41249  cdlemk16-2N  41250  cdlemk17-2N  41251  cdlemk18-2N  41256  cdlemk19-2N  41257  cdlemk7u-2N  41258  cdlemk11u-2N  41259  cdlemk20-2N  41262  cdlemk30  41264  cdlemk23-3  41272  cdlemk24-3  41273