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

Theorem mtand 655
Description: A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
Hypotheses
Ref Expression
mtand.1  |-  ( ph  ->  -.  ch )
mtand.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mtand  |-  ( ph  ->  -.  ps )

Proof of Theorem mtand
StepHypRef Expression
1 mtand.1 . 2  |-  ( ph  ->  -.  ch )
2 mtand.2 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
32ex 114 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 3mtod 653 1  |-  ( ph  ->  -.  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107  ax-in1 604  ax-in2 605
This theorem is referenced by:  frirrg  4323  phpm  6823  diffisn  6851  tridc  6857  nnnninfeq  7084  pm54.43  7138  addcanprleml  7547  addcanprlemu  7548  iseqf1olemklt  10411  isprm5lem  12062  pw2dvdseulemle  12088  sqne2sq  12098  pythagtriplem4  12189  pythagtriplem11  12195  pythagtriplem13  12197  ctinfomlemom  12323  ivthinc  13188  pwle2  13740
  Copyright terms: Public domain W3C validator