![]() |
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 2756 cesaroOLD 2764 pwnss 5052 reusv2lem2 5099 reldmtpos 7625 tz7.49 7806 omopthlem2 8003 domnsym 8355 sdomirr 8366 infensuc 8407 fofinf1o 8510 elfi2 8589 infdifsn 8831 carden2b 9106 alephsucdom 9215 infdif2 9347 fin4i 9435 bitsf1 15541 pcmpt2 15968 ufinffr 22103 eldmgm 25161 lgamucov 25177 facgam 25205 chtub 25350 lfgrnloop 26423 umgredgnlp 26446 clwwlkn0 27370 eupth2lem1 27595 oddpwdc 30961 bnj1312 31672 erdszelem10 31728 heiborlem1 34152 osumcllem4N 36034 pexmidlem1N 36045 fphpd 38224 0nodd 42657 |
Copyright terms: Public domain | W3C validator |