ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nsyl3 GIF version

Theorem nsyl3 626
Description: A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) (Revised by NM, 13-Jun-2013.)
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 9 . 2 (𝜒 → (𝜑 → ¬ 𝜓))
41, 3mt2d 625 1 (𝜒 → ¬ 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 614  ax-in2 615
This theorem is referenced by:  con2i  627  nsyl  628  pm2.65i  639  cesare  2130  cesaro  2134  pwnss  4160  sucprcreg  4549  reg3exmidlemwe  4579  reldmtpos  6254  snexxph  6949  elfi2  6971  ismkvnex  7153  fzn  10042  seq3f1olemqsum  10500  pcmpt2  12342
  Copyright terms: Public domain W3C validator