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 5216 reusv2lem2 5266 reldmtpos 7929 tz7.49 8110 omopthlem2 8314 domnsym 8693 sdomirr 8704 infensuc 8745 fofinf1o 8872 elfi2 8951 infdifsn 9193 carden2b 9469 alephsucdom 9579 infdif2 9710 fin4i 9798 fin45 9892 bitsf1 15889 pcmpt2 16329 symgvalstruct 18643 ufinffr 22680 eldmgm 25759 lgamucov 25775 facgam 25803 chtub 25948 lfgrnloop 27070 umgredgnlp 27092 clwwlkn0 27965 eupth2lem1 28155 oddpwdc 31891 bnj1312 32609 erdszelem10 32733 cofcutr 33730 heiborlem1 35592 osumcllem4N 37596 pexmidlem1N 37607 fphpd 40210 0nodd 44898 |
Copyright terms: Public domain | W3C validator |