| 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 5352 reusv2lem2 5399 reldmtpos 8259 tz7.49 8485 omopthlem2 8698 domnsym 9139 sdomirr 9154 infensuc 9195 domnsymfi 9240 fofinf1o 9372 elfi2 9454 infdifsn 9697 carden2b 10007 alephsucdom 10119 infdif2 10249 fin4i 10338 fin45 10432 bitsf1 16483 pcmpt2 16931 symgvalstruct 19414 symgvalstructOLD 19415 ufinffr 23937 eldmgm 27065 lgamucov 27081 facgam 27109 chtub 27256 cuteq1 27878 cofcutr 27958 lfgrnloop 29142 umgredgnlp 29164 clwwlkn0 30047 eupth2lem1 30237 rtelextdg2lem 33767 oddpwdc 34356 bnj1312 35072 erdszelem10 35205 heiborlem1 37818 osumcllem4N 39961 pexmidlem1N 39972 fimgmcyc 42544 fphpd 42827 0nodd 48086 |
| Copyright terms: Public domain | W3C validator |