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  5216  reusv2lem2  5266  reldmtpos  7929  tz7.49  8110  omopthlem2  8314  domnsym  8693  sdomirr  8704  infensuc  8745  fofinf1o  8872  elfi2  8951  infdifsn  9193  carden2b  9469  alephsucdom  9579  infdif2  9710  fin4i  9798  fin45  9892  bitsf1  15889  pcmpt2  16329  symgvalstruct  18643  ufinffr  22680  eldmgm  25759  lgamucov  25775  facgam  25803  chtub  25948  lfgrnloop  27070  umgredgnlp  27092  clwwlkn0  27965  eupth2lem1  28155  oddpwdc  31891  bnj1312  32609  erdszelem10  32733  cofcutr  33730  heiborlem1  35592  osumcllem4N  37596  pexmidlem1N  37607  fphpd  40210  0nodd  44898
  Copyright terms: Public domain W3C validator