![]() |
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 161 | . 2 ⊢ (¬ 𝜒 → 𝜓) |
4 | 3 | con1i 149 | 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 2634 moanimlem 2640 moexexlem 2648 eueq3 3622 opprc1 4780 opprc2 4781 mosubopt 5362 nfvres 6687 fvco4i 6746 fvmptex 6766 fvopab4ndm 6781 ressnop0 6899 csbriota 7116 ovprc 7181 ovprc1 7182 ovprc2 7183 ndmovass 7325 ndmovdistr 7326 extmptsuppeq 7855 funsssuppss 7857 eceqoveq 8405 supval2 8937 axpowndlem3 10044 adderpq 10401 mulerpq 10402 fzoval 13073 swrdnznd 14036 pfxnd0 14082 grpidval 17922 tgdif0 21677 resstopn 21871 rdgprc0 33270 bj-projval 34698 wl-nax6im 35188 itg2addnclem3 35375 or3or 41082 ndmafv 44049 nfunsnafv 44051 afvnufveq 44056 aovprc 44097 ndmaovass 44115 ndmaovdistr 44116 tz6.12-2-afv2 44146 naryfval 45392 naryfvalixp 45393 |
Copyright terms: Public domain | W3C validator |