ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nsyl3 Unicode 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  |-  ( 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 625 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 614  ax-in2 615
This theorem is referenced by:  con2i  627  nsyl  628  pm2.65i  639  cesare  2130  cesaro  2134  pwnss  4161  sucprcreg  4550  reg3exmidlemwe  4580  reldmtpos  6257  snexxph  6952  elfi2  6974  ismkvnex  7156  fzn  10045  seq3f1olemqsum  10503  pcmpt2  12345
  Copyright terms: Public domain W3C validator