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 138 | 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 141 nsyl 142 nsyl2 143 pwnss 5241 reusv2lem2 5290 reldmtpos 7889 tz7.49 8070 omopthlem2 8272 domnsym 8631 sdomirr 8642 infensuc 8683 fofinf1o 8787 elfi2 8866 infdifsn 9108 carden2b 9384 alephsucdom 9493 infdif2 9620 fin4i 9708 fin45 9802 bitsf1 15783 pcmpt2 16217 ufinffr 22465 eldmgm 25526 lgamucov 25542 facgam 25570 chtub 25715 lfgrnloop 26837 umgredgnlp 26859 clwwlkn0 27733 eupth2lem1 27924 oddpwdc 31511 bnj1312 32227 erdszelem10 32344 heiborlem1 34970 osumcllem4N 36975 pexmidlem1N 36986 fphpd 39291 0nodd 43954 |
Copyright terms: Public domain | W3C validator |