Theorem mtoi 670

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 669	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 619  ax-in2 620

This theorem is referenced by:  mtbii  680  mtbiri  681  pwnss  4249  exmid1stab  4298  nsuceq0g  4515  abnex  4544  reg2exmidlema  4632  ordsuc  4661  onnmin  4666  ssnel  4667  ordtri2or2exmid  4669  ontri2orexmidim  4670  reg3exmidlemwe  4677  acexmidlemab  6012  reldmtpos  6419  dmtpos  6422  2pwuninelg  6449  onunsnss  7109  snon0  7134  nninfisol  7332  exmidomni  7341  pr2ne  7397  ltexprlemdisj  7826  recexprlemdisj  7850  caucvgprlemnkj  7886  caucvgprprlemnkltj  7909  caucvgprprlemnkeqj  7910  caucvgprprlemnjltk  7911  inelr  8764  rimul  8765  recgt0  9030  zfz1iso  11105  isprm2  12690  nprmdvds1  12713  divgcdodd  12716  coprm  12717  coseq0q4123  15560  lgsquad2lem2  15813  umgrnloop0  15970  umgrislfupgrenlem  15983  lfgrnloopen  15986  3dom  16590  pwle2  16602  nninfalllem1  16613  nninfall  16614  nninfsellemqall  16620