Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nsyl3 | Structured version Visualization version GIF version |
Description: A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) |
Ref | Expression |
---|---|
nsyl3.1 | ⊢ (𝜑 → ¬ 𝜓) |
nsyl3.2 | ⊢ (𝜒 → 𝜓) |
Ref | Expression |
---|---|
nsyl3 | ⊢ (𝜒 → ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nsyl3.2 | . 2 ⊢ (𝜒 → 𝜓) | |
2 | nsyl3.1 | . . 3 ⊢ (𝜑 → ¬ 𝜓) | |
3 | 2 | a1i 11 | . 2 ⊢ (𝜒 → (𝜑 → ¬ 𝜓)) |
4 | 1, 3 | mt2d 130 | 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: con2i 133 nsyl 134 cesare 2557 cesaro 2561 pwnss 4756 reusv2lem2 4795 reusv2lem2OLD 4796 reldmtpos 7247 tz7.49 7427 omopthlem2 7623 domnsym 7971 sdomirr 7982 infensuc 8023 fofinf1o 8126 elfi2 8203 infdifsn 8437 carden2b 8676 alephsucdom 8785 infdif2 8915 fin4i 9003 bitsf1 15006 pcmpt2 15435 ufinffr 21543 eldmgm 24548 lgamucov 24564 facgam 24592 chtub 24737 lfgrnloop 25791 umgredgnlp 25818 eupath2lem1 26504 oddpwdc 29743 bnj1312 30380 erdszelem10 30436 heiborlem1 32780 osumcllem4N 34263 pexmidlem1N 34274 fphpd 36398 eupth2lem1 41386 0nodd 41600 |
Copyright terms: Public domain | W3C validator |