MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nsyl3 Structured version   Visualization version   GIF version

Theorem nsyl3 140
Description: A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
Hypotheses
Ref Expression
nsyl3.1 (𝜑 → ¬ 𝜓)
nsyl3.2 (𝜒𝜓)
Assertion
Ref Expression
nsyl3 (𝜒 → ¬ 𝜑)

Proof of Theorem nsyl3
StepHypRef Expression
1 nsyl3.2 . 2 (𝜒𝜓)
2 nsyl3.1 . . 3 (𝜑 → ¬ 𝜓)
32a1i 11 . 2 (𝜒 → (𝜑 → ¬ 𝜓))
41, 3mt2d 138 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  141  nsyl  142  nsyl2  143  pwnss  5241  reusv2lem2  5290  reldmtpos  7889  tz7.49  8070  omopthlem2  8272  domnsym  8631  sdomirr  8642  infensuc  8683  fofinf1o  8787  elfi2  8866  infdifsn  9108  carden2b  9384  alephsucdom  9493  infdif2  9620  fin4i  9708  fin45  9802  bitsf1  15783  pcmpt2  16217  ufinffr  22465  eldmgm  25526  lgamucov  25542  facgam  25570  chtub  25715  lfgrnloop  26837  umgredgnlp  26859  clwwlkn0  27733  eupth2lem1  27924  oddpwdc  31511  bnj1312  32227  erdszelem10  32344  heiborlem1  34970  osumcllem4N  36975  pexmidlem1N  36986  fphpd  39291  0nodd  43954
  Copyright terms: Public domain W3C validator