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  40941  paddasslem15  40984  4atex2-0aOLDN  41228  4atex3  41231  trlval3  41337  cdleme12  41421  cdleme19b  41454  cdleme19d  41456  cdleme19e  41457  cdleme20d  41462  cdleme20f  41464  cdleme20g  41465  cdleme21d  41480  cdleme21e  41481  cdleme21f  41482  cdleme22cN  41492  cdleme22e  41494  cdleme22f2  41497  cdleme22g  41498  cdleme26e  41509  cdleme28a  41520  cdleme37m  41612  cdleme39n  41616  cdlemg28b  41853  cdlemk3  41983  cdlemk12  42000  cdlemk12u  42022  cdlemkoatnle-2N  42025  cdlemk13-2N  42026  cdlemkole-2N  42027  cdlemk14-2N  42028  cdlemk15-2N  42029  cdlemk16-2N  42030  cdlemk17-2N  42031  cdlemk18-2N  42036  cdlemk19-2N  42037  cdlemk7u-2N  42038  cdlemk11u-2N  42039  cdlemk20-2N  42042  cdlemk30  42044  cdlemk23-3  42052  cdlemk24-3  42053