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  39785  paddasslem15  39828  4atex2-0aOLDN  40072  4atex3  40075  trlval3  40181  cdleme12  40265  cdleme19b  40298  cdleme19d  40300  cdleme19e  40301  cdleme20d  40306  cdleme20f  40308  cdleme20g  40309  cdleme21d  40324  cdleme21e  40325  cdleme21f  40326  cdleme22cN  40336  cdleme22e  40338  cdleme22f2  40341  cdleme22g  40342  cdleme26e  40353  cdleme28a  40364  cdleme37m  40456  cdleme39n  40460  cdlemg28b  40697  cdlemk3  40827  cdlemk12  40844  cdlemk12u  40866  cdlemkoatnle-2N  40869  cdlemk13-2N  40870  cdlemkole-2N  40871  cdlemk14-2N  40872  cdlemk15-2N  40873  cdlemk16-2N  40874  cdlemk17-2N  40875  cdlemk18-2N  40880  cdlemk19-2N  40881  cdlemk7u-2N  40882  cdlemk11u-2N  40883  cdlemk20-2N  40886  cdlemk30  40888  cdlemk23-3  40896  cdlemk24-3  40897