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  6015  reldmtpos  6422  dmtpos  6425  2pwuninelg  6452  onunsnss  7112  snon0  7137  nninfisol  7335  exmidomni  7344  pr2ne  7400  ltexprlemdisj  7829  recexprlemdisj  7853  caucvgprlemnkj  7889  caucvgprprlemnkltj  7912  caucvgprprlemnkeqj  7913  caucvgprprlemnjltk  7914  inelr  8767  rimul  8768  recgt0  9033  zfz1iso  11109  isprm2  12710  nprmdvds1  12733  divgcdodd  12736  coprm  12737  coseq0q4123  15585  lgsquad2lem2  15838  umgrnloop0  15995  umgrislfupgrenlem  16008  lfgrnloopen  16011  3dom  16646  pwle2  16658  nninfalllem1  16669  nninfall  16670  nninfsellemqall  16676