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 136 | 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 139 nsyl 140 nsyl2 141 pwnss 5272 reusv2lem2 5322 reldmtpos 8050 tz7.49 8276 omopthlem2 8490 domnsym 8886 sdomirr 8901 infensuc 8942 domnsymfi 8986 fofinf1o 9094 elfi2 9173 infdifsn 9415 carden2b 9725 alephsucdom 9835 infdif2 9966 fin4i 10054 fin45 10148 bitsf1 16153 pcmpt2 16594 symgvalstruct 19004 symgvalstructOLD 19005 ufinffr 23080 eldmgm 26171 lgamucov 26187 facgam 26215 chtub 26360 lfgrnloop 27495 umgredgnlp 27517 clwwlkn0 28392 eupth2lem1 28582 oddpwdc 32321 bnj1312 33038 erdszelem10 33162 cofcutr 34092 heiborlem1 35969 osumcllem4N 37973 pexmidlem1N 37984 fphpd 40638 0nodd 45364 |
Copyright terms: Public domain | W3C validator |