| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nsyl5 | Structured version Visualization version GIF version | ||
| Description: A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024.) |
| Ref | Expression |
|---|---|
| nsyl4.1 | ⊢ (𝜑 → 𝜓) |
| nsyl4.2 | ⊢ (¬ 𝜑 → 𝜒) |
| Ref | Expression |
|---|---|
| nsyl5 | ⊢ (¬ 𝜓 → 𝜒) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nsyl4.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
| 2 | nsyl4.2 | . . 3 ⊢ (¬ 𝜑 → 𝜒) | |
| 3 | 1, 2 | nsyl4 158 | . 2 ⊢ (¬ 𝜒 → 𝜓) |
| 4 | 3 | con1i 147 | 1 ⊢ (¬ 𝜓 → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem is referenced by: pm5.55 951 euor2 2613 moanimlem 2618 moexexlem 2626 eueq3 3717 opprc1 4897 opprc2 4898 mosubopt 5515 nfvres 6947 fvco4i 7010 fvmptex 7030 fvopab4ndm 7046 ressnop0 7173 csbriota 7403 ovprc 7469 ovprc1 7470 ovprc2 7471 ndmovass 7621 ndmovdistr 7622 extmptsuppeq 8213 funsssuppss 8215 eceqoveq 8862 supval2 9495 axpowndlem3 10639 adderpq 10996 mulerpq 10997 fzoval 13700 swrdnznd 14680 pfxnd0 14726 grpidval 18674 tgdif0 22999 resstopn 23194 prcinf 35108 rdgprc0 35794 bj-projval 36997 wl-nax6im 37519 itg2addnclem3 37680 or3or 44036 ndmafv 47152 nfunsnafv 47154 afvnufveq 47159 aovprc 47200 ndmaovass 47218 ndmaovdistr 47219 tz6.12-2-afv2 47249 naryfval 48549 naryfvalixp 48550 |
| Copyright terms: Public domain | W3C validator |