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  39792  paddasslem15  39835  4atex2-0aOLDN  40079  4atex3  40082  trlval3  40188  cdleme12  40272  cdleme19b  40305  cdleme19d  40307  cdleme19e  40308  cdleme20d  40313  cdleme20f  40315  cdleme20g  40316  cdleme21d  40331  cdleme21e  40332  cdleme21f  40333  cdleme22cN  40343  cdleme22e  40345  cdleme22f2  40348  cdleme22g  40349  cdleme26e  40360  cdleme28a  40371  cdleme37m  40463  cdleme39n  40467  cdlemg28b  40704  cdlemk3  40834  cdlemk12  40851  cdlemk12u  40873  cdlemkoatnle-2N  40876  cdlemk13-2N  40877  cdlemkole-2N  40878  cdlemk14-2N  40879  cdlemk15-2N  40880  cdlemk16-2N  40881  cdlemk17-2N  40882  cdlemk18-2N  40887  cdlemk19-2N  40888  cdlemk7u-2N  40889  cdlemk11u-2N  40890  cdlemk20-2N  40893  cdlemk30  40895  cdlemk23-3  40903  cdlemk24-3  40904