![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simp32r | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp32r | ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2r 1198 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓) | |
2 | 1 | 3ad2ant3 1133 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 396 df-3an 1087 |
This theorem is referenced by: cdlema1N 39201 paddasslem15 39244 4atex2-0aOLDN 39488 4atex3 39491 cdleme19b 39714 cdleme19d 39716 cdleme19e 39717 cdleme20d 39722 cdleme20f 39724 cdleme20g 39725 cdleme21d 39740 cdleme21e 39741 cdleme22cN 39752 cdleme22e 39754 cdleme22f2 39757 cdleme26e 39769 cdleme28a 39780 cdleme37m 39872 cdlemg28b 40113 cdlemk3 40243 cdlemk12 40260 cdlemk12u 40282 cdlemkoatnle-2N 40285 cdlemk13-2N 40286 cdlemkole-2N 40287 cdlemk14-2N 40288 cdlemk15-2N 40289 cdlemk16-2N 40290 cdlemk17-2N 40291 cdlemk18-2N 40296 cdlemk19-2N 40297 cdlemk7u-2N 40298 cdlemk11u-2N 40299 cdlemk20-2N 40302 cdlemk30 40304 cdlemk23-3 40312 cdlemk24-3 40313 |
Copyright terms: Public domain | W3C validator |