ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nsyl3 Unicode 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  |-  ( ph  ->  -.  ps )
nsyl3.2  |-  ( ch 
->  ps )
Assertion
Ref Expression
nsyl3  |-  ( ch 
->  -.  ph )

Proof of Theorem nsyl3
StepHypRef Expression
1 nsyl3.2 . 2  |-  ( ch 
->  ps )
2 nsyl3.1 . . 3  |-  ( ph  ->  -.  ps )
32a1i 9 . 2  |-  ( ch 
->  ( ph  ->  -.  ps ) )
41, 3mt2d 626 1  |-  ( ch 
->  -.  ph )
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  2141  cesaro  2145  pwnss  4173  sucprcreg  4562  reg3exmidlemwe  4592  reldmtpos  6271  snexxph  6966  elfi2  6988  ismkvnex  7170  fzn  10059  seq3f1olemqsum  10517  pcmpt2  12359
  Copyright terms: Public domain W3C validator