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  40672  paddasslem15  40715  4atex2-0aOLDN  40959  4atex3  40962  trlval3  41068  cdleme12  41152  cdleme19b  41185  cdleme19d  41187  cdleme19e  41188  cdleme20d  41193  cdleme20f  41195  cdleme20g  41196  cdleme21d  41211  cdleme21e  41212  cdleme21f  41213  cdleme22cN  41223  cdleme22e  41225  cdleme22f2  41228  cdleme22g  41229  cdleme26e  41240  cdleme28a  41251  cdleme37m  41343  cdleme39n  41347  cdlemg28b  41584  cdlemk3  41714  cdlemk12  41731  cdlemk12u  41753  cdlemkoatnle-2N  41756  cdlemk13-2N  41757  cdlemkole-2N  41758  cdlemk14-2N  41759  cdlemk15-2N  41760  cdlemk16-2N  41761  cdlemk17-2N  41762  cdlemk18-2N  41767  cdlemk19-2N  41768  cdlemk7u-2N  41769  cdlemk11u-2N  41770  cdlemk20-2N  41773  cdlemk30  41775  cdlemk23-3  41783  cdlemk24-3  41784