Theorem simp32l 1186

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

Assertion

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

Proof of Theorem simp32l

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  cdlema1N  35077  paddasslem15  35120  4atex2-0aOLDN  35364  4atex3  35367  trlval3  35474  cdleme12  35558  cdleme19b  35592  cdleme19d  35594  cdleme19e  35595  cdleme20d  35600  cdleme20f  35602  cdleme20g  35603  cdleme21d  35618  cdleme21e  35619  cdleme21f  35620  cdleme22cN  35630  cdleme22e  35632  cdleme22f2  35635  cdleme22g  35636  cdleme26e  35647  cdleme28a  35658  cdleme37m  35750  cdleme39n  35754  cdlemg28b  35991  cdlemk3  36121  cdlemk12  36138  cdlemk12u  36160  cdlemkoatnle-2N  36163  cdlemk13-2N  36164  cdlemkole-2N  36165  cdlemk14-2N  36166  cdlemk15-2N  36167  cdlemk16-2N  36168  cdlemk17-2N  36169  cdlemk18-2N  36174  cdlemk19-2N  36175  cdlemk7u-2N  36176  cdlemk11u-2N  36177  cdlemk20-2N  36180  cdlemk30  36182  cdlemk23-3  36190  cdlemk24-3  36191