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

Theorem mtoi 665
Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
Hypotheses
Ref Expression
mtoi.1  |-  -.  ch
mtoi.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mtoi  |-  ( ph  ->  -.  ps )

Proof of Theorem mtoi
StepHypRef Expression
1 mtoi.1 . . 3  |-  -.  ch
21a1i 9 . 2  |-  ( ph  ->  -.  ch )
3 mtoi.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3mtod 664 1  |-  ( ph  ->  -.  ps )
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:  mtbii  675  mtbiri  676  pwnss  4189  exmid1stab  4238  nsuceq0g  4450  abnex  4479  reg2exmidlema  4567  ordsuc  4596  onnmin  4601  ssnel  4602  ordtri2or2exmid  4604  ontri2orexmidim  4605  reg3exmidlemwe  4612  acexmidlemab  5913  reldmtpos  6308  dmtpos  6311  2pwuninelg  6338  onunsnss  6975  snon0  6996  nninfisol  7194  exmidomni  7203  pr2ne  7254  ltexprlemdisj  7668  recexprlemdisj  7692  caucvgprlemnkj  7728  caucvgprprlemnkltj  7751  caucvgprprlemnkeqj  7752  caucvgprprlemnjltk  7753  inelr  8605  rimul  8606  recgt0  8871  zfz1iso  10915  isprm2  12258  nprmdvds1  12281  divgcdodd  12284  coprm  12285  coseq0q4123  15010  lgsquad2lem2  15239  pwle2  15559  nninfalllem1  15568  nninfall  15569  nninfsellemqall  15575
  Copyright terms: Public domain W3C validator