![]() |
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 1199 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜑) | |
2 | 1 | 3ad2ant3 1135 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 |
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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: cdlema1N 38467 paddasslem15 38510 4atex2-0aOLDN 38754 4atex3 38757 trlval3 38863 cdleme12 38947 cdleme19b 38980 cdleme19d 38982 cdleme19e 38983 cdleme20d 38988 cdleme20f 38990 cdleme20g 38991 cdleme21d 39006 cdleme21e 39007 cdleme21f 39008 cdleme22cN 39018 cdleme22e 39020 cdleme22f2 39023 cdleme22g 39024 cdleme26e 39035 cdleme28a 39046 cdleme37m 39138 cdleme39n 39142 cdlemg28b 39379 cdlemk3 39509 cdlemk12 39526 cdlemk12u 39548 cdlemkoatnle-2N 39551 cdlemk13-2N 39552 cdlemkole-2N 39553 cdlemk14-2N 39554 cdlemk15-2N 39555 cdlemk16-2N 39556 cdlemk17-2N 39557 cdlemk18-2N 39562 cdlemk19-2N 39563 cdlemk7u-2N 39564 cdlemk11u-2N 39565 cdlemk20-2N 39568 cdlemk30 39570 cdlemk23-3 39578 cdlemk24-3 39579 |
Copyright terms: Public domain | W3C validator |