![]() |
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 5339 reusv2lem2 5387 reldmtpos 8214 tz7.49 8440 omopthlem2 8655 domnsym 9095 sdomirr 9110 infensuc 9151 domnsymfi 9199 fofinf1o 9323 elfi2 9405 infdifsn 9648 carden2b 9958 alephsucdom 10070 infdif2 10201 fin4i 10289 fin45 10383 bitsf1 16384 pcmpt2 16825 symgvalstruct 19306 symgvalstructOLD 19307 ufinffr 23755 eldmgm 26870 lgamucov 26886 facgam 26914 chtub 27061 cuteq1 27682 cofcutr 27760 lfgrnloop 28854 umgredgnlp 28876 clwwlkn0 29750 eupth2lem1 29940 oddpwdc 33842 bnj1312 34558 erdszelem10 34680 heiborlem1 37169 osumcllem4N 39320 pexmidlem1N 39331 fphpd 42043 0nodd 47033 |
Copyright terms: Public domain | W3C validator |