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

Theorem nsyl3 627
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 626 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 615  ax-in2 616
This theorem is referenced by:  con2i  628  nsyl  629  pm2.65i  640  cesare  2157  cesaro  2161  pwnss  4202  sucprcreg  4596  reg3exmidlemwe  4626  reldmtpos  6338  snexxph  7051  elfi2  7073  ismkvnex  7256  fzn  10163  seq3f1olemqsum  10656  pcmpt2  12638  elply2  15178
  Copyright terms: Public domain W3C validator