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 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  cdlema1N  40543  paddasslem15  40586  4atex2-0aOLDN  40830  4atex3  40833  trlval3  40939  cdleme12  41023  cdleme19b  41056  cdleme19d  41058  cdleme19e  41059  cdleme20d  41064  cdleme20f  41066  cdleme20g  41067  cdleme21d  41082  cdleme21e  41083  cdleme21f  41084  cdleme22cN  41094  cdleme22e  41096  cdleme22f2  41099  cdleme22g  41100  cdleme26e  41111  cdleme28a  41122  cdleme37m  41214  cdleme39n  41218  cdlemg28b  41455  cdlemk3  41585  cdlemk12  41602  cdlemk12u  41624  cdlemkoatnle-2N  41627  cdlemk13-2N  41628  cdlemkole-2N  41629  cdlemk14-2N  41630  cdlemk15-2N  41631  cdlemk16-2N  41632  cdlemk17-2N  41633  cdlemk18-2N  41638  cdlemk19-2N  41639  cdlemk7u-2N  41640  cdlemk11u-2N  41641  cdlemk20-2N  41644  cdlemk30  41646  cdlemk23-3  41654  cdlemk24-3  41655