![]() |
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 134 | 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 137 nsyl 138 cesareOLD 2757 cesaroOLD 2765 pwnss 5053 reusv2lem2 5100 reldmtpos 7626 tz7.49 7807 omopthlem2 8004 domnsym 8356 sdomirr 8367 infensuc 8408 fofinf1o 8511 elfi2 8590 infdifsn 8832 carden2b 9107 alephsucdom 9216 infdif2 9348 fin4i 9436 bitsf1 15542 pcmpt2 15969 ufinffr 22104 eldmgm 25162 lgamucov 25178 facgam 25206 chtub 25351 lfgrnloop 26424 umgredgnlp 26447 clwwlkn0 27371 eupth2lem1 27596 oddpwdc 30962 bnj1312 31673 erdszelem10 31729 heiborlem1 34153 osumcllem4N 36035 pexmidlem1N 36046 fphpd 38225 0nodd 42658 |
Copyright terms: Public domain | W3C validator |