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  40047  paddasslem15  40090  4atex2-0aOLDN  40334  4atex3  40337  trlval3  40443  cdleme12  40527  cdleme19b  40560  cdleme19d  40562  cdleme19e  40563  cdleme20d  40568  cdleme20f  40570  cdleme20g  40571  cdleme21d  40586  cdleme21e  40587  cdleme21f  40588  cdleme22cN  40598  cdleme22e  40600  cdleme22f2  40603  cdleme22g  40604  cdleme26e  40615  cdleme28a  40626  cdleme37m  40718  cdleme39n  40722  cdlemg28b  40959  cdlemk3  41089  cdlemk12  41106  cdlemk12u  41128  cdlemkoatnle-2N  41131  cdlemk13-2N  41132  cdlemkole-2N  41133  cdlemk14-2N  41134  cdlemk15-2N  41135  cdlemk16-2N  41136  cdlemk17-2N  41137  cdlemk18-2N  41142  cdlemk19-2N  41143  cdlemk7u-2N  41144  cdlemk11u-2N  41145  cdlemk20-2N  41148  cdlemk30  41150  cdlemk23-3  41158  cdlemk24-3  41159