| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > simp31r | Structured version Visualization version GIF version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| Ref | Expression |
|---|---|
| simp31r | ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simp1r 1199 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | |
| 2 | 1 | 3ad2ant3 1136 | 1 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: ps-2c 39530 cdlema1N 39793 cdlemednpq 40301 cdleme19e 40309 cdleme20h 40318 cdleme20j 40320 cdleme20l2 40323 cdleme20m 40325 cdleme22a 40342 cdleme22cN 40344 cdleme22f2 40349 cdleme26f2ALTN 40366 cdleme37m 40464 cdlemg12f 40650 cdlemg12g 40651 cdlemg12 40652 cdlemg28a 40695 cdlemg29 40707 cdlemg33a 40708 cdlemg36 40716 cdlemk16a 40858 cdlemk21-2N 40893 cdlemk54 40960 dihord10 41225 |
| Copyright terms: Public domain | W3C validator |