Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp32l | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp32l | ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2l 1080 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜑) | |
2 | 1 | 3ad2ant3 1077 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: cdlema1N 34095 paddasslem15 34138 4atex2-0aOLDN 34382 4atex3 34385 trlval3 34492 cdleme12 34576 cdleme19b 34610 cdleme19d 34612 cdleme19e 34613 cdleme20d 34618 cdleme20f 34620 cdleme20g 34621 cdleme21d 34636 cdleme21e 34637 cdleme21f 34638 cdleme22cN 34648 cdleme22e 34650 cdleme22f2 34653 cdleme22g 34654 cdleme26e 34665 cdleme28a 34676 cdleme37m 34768 cdleme39n 34772 cdlemg28b 35009 cdlemk3 35139 cdlemk12 35156 cdlemk12u 35178 cdlemkoatnle-2N 35181 cdlemk13-2N 35182 cdlemkole-2N 35183 cdlemk14-2N 35184 cdlemk15-2N 35185 cdlemk16-2N 35186 cdlemk17-2N 35187 cdlemk18-2N 35192 cdlemk19-2N 35193 cdlemk7u-2N 35194 cdlemk11u-2N 35195 cdlemk20-2N 35198 cdlemk30 35200 cdlemk23-3 35208 cdlemk24-3 35209 |
Copyright terms: Public domain | W3C validator |