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

Theorem nsyl3 136
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 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