Theorem mtoi 674

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

Step	Hyp	Ref	Expression
1		mtoi.1	. . 3 |- -. ch
2	1	a1i 9	. 2 |- ( ph -> -. ch )
3		mtoi.2	. 2 |- ( ph -> ( ps -> ch ) )
4	2, 3	mtod 673	1 |- ( ph -> -. ps )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is referenced by:  mtbii  685  mtbiri  686  ifeqeqxdc  3687  pwnss  4294  exmid1stab  4343  nsuceq0g  4561  abnex  4591  reg2exmidlema  4679  ordsuc  4708  onnmin  4713  ssnel  4714  ordtri2or2exmid  4716  ontri2orexmidim  4717  reg3exmidlemwe  4724  acexmidlemab  6072  reldmtpos  6517  dmtpos  6520  2pwuninelg  6547  onunsnss  7217  snon0  7242  nninfisol  7466  exmidomni  7475  pr2ne  7531  ltexprlemdisj  7966  recexprlemdisj  7990  caucvgprlemnkj  8026  caucvgprprlemnkltj  8049  caucvgprprlemnkeqj  8050  caucvgprprlemnjltk  8051  inelr  8905  rimul  8906  recgt0  9173  zfz1iso  11274  isprm2  12876  nprmdvds1  12899  divgcdodd  12902  coprm  12903  coseq0q4123  15861  lgsquad2lem2  16118  umgrnloop0  16275  umgrislfupgrenlem  16288  lfgrnloopen  16291  3dom  16935  pwle2  16945  nninfalllem1  16959  nninfall  16960  nninfsellemqall  16966