Theorem simp32l 1295

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

Assertion

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

Proof of Theorem simp32l

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  cdlema1N  37087  paddasslem15  37130  4atex2-0aOLDN  37374  4atex3  37377  trlval3  37483  cdleme12  37567  cdleme19b  37600  cdleme19d  37602  cdleme19e  37603  cdleme20d  37608  cdleme20f  37610  cdleme20g  37611  cdleme21d  37626  cdleme21e  37627  cdleme21f  37628  cdleme22cN  37638  cdleme22e  37640  cdleme22f2  37643  cdleme22g  37644  cdleme26e  37655  cdleme28a  37666  cdleme37m  37758  cdleme39n  37762  cdlemg28b  37999  cdlemk3  38129  cdlemk12  38146  cdlemk12u  38168  cdlemkoatnle-2N  38171  cdlemk13-2N  38172  cdlemkole-2N  38173  cdlemk14-2N  38174  cdlemk15-2N  38175  cdlemk16-2N  38176  cdlemk17-2N  38177  cdlemk18-2N  38182  cdlemk19-2N  38183  cdlemk7u-2N  38184  cdlemk11u-2N  38185  cdlemk20-2N  38188  cdlemk30  38190  cdlemk23-3  38198  cdlemk24-3  38199