![]() |
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 947 euor2 2609 moanimlem 2614 moexexlem 2622 eueq3 3706 opprc1 4896 opprc2 4897 mosubopt 5509 nfvres 6929 fvco4i 6989 fvmptex 7009 fvopab4ndm 7024 ressnop0 7147 csbriota 7377 ovprc 7443 ovprc1 7444 ovprc2 7445 ndmovass 7591 ndmovdistr 7592 extmptsuppeq 8169 funsssuppss 8171 eceqoveq 8812 supval2 9446 axpowndlem3 10590 adderpq 10947 mulerpq 10948 fzoval 13629 swrdnznd 14588 pfxnd0 14634 grpidval 18576 tgdif0 22486 resstopn 22681 rdgprc0 34753 bj-projval 35865 wl-nax6im 36375 itg2addnclem3 36529 or3or 42759 ndmafv 45834 nfunsnafv 45836 afvnufveq 45841 aovprc 45882 ndmaovass 45900 ndmaovdistr 45901 tz6.12-2-afv2 45931 naryfval 47267 naryfvalixp 47268 |
Copyright terms: Public domain | W3C validator |