Theorem simp32l 1299

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

Assertion

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

Proof of Theorem simp32l

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

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

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 1088

This theorem is referenced by:  cdlema1N  39829  paddasslem15  39872  4atex2-0aOLDN  40116  4atex3  40119  trlval3  40225  cdleme12  40309  cdleme19b  40342  cdleme19d  40344  cdleme19e  40345  cdleme20d  40350  cdleme20f  40352  cdleme20g  40353  cdleme21d  40368  cdleme21e  40369  cdleme21f  40370  cdleme22cN  40380  cdleme22e  40382  cdleme22f2  40385  cdleme22g  40386  cdleme26e  40397  cdleme28a  40408  cdleme37m  40500  cdleme39n  40504  cdlemg28b  40741  cdlemk3  40871  cdlemk12  40888  cdlemk12u  40910  cdlemkoatnle-2N  40913  cdlemk13-2N  40914  cdlemkole-2N  40915  cdlemk14-2N  40916  cdlemk15-2N  40917  cdlemk16-2N  40918  cdlemk17-2N  40919  cdlemk18-2N  40924  cdlemk19-2N  40925  cdlemk7u-2N  40926  cdlemk11u-2N  40927  cdlemk20-2N  40930  cdlemk30  40932  cdlemk23-3  40940  cdlemk24-3  40941