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  681  mtbiri  682  pwnss  4274  exmid1stab  4323  nsuceq0g  4541  abnex  4570  reg2exmidlema  4658  ordsuc  4687  onnmin  4692  ssnel  4693  ordtri2or2exmid  4695  ontri2orexmidim  4696  reg3exmidlemwe  4703  acexmidlemab  6046  reldmtpos  6486  dmtpos  6489  2pwuninelg  6516  onunsnss  7179  snon0  7204  nninfisol  7426  exmidomni  7435  pr2ne  7491  ltexprlemdisj  7923  recexprlemdisj  7947  caucvgprlemnkj  7983  caucvgprprlemnkltj  8006  caucvgprprlemnkeqj  8007  caucvgprprlemnjltk  8008  inelr  8860  rimul  8861  recgt0  9126  zfz1iso  11217  isprm2  12818  nprmdvds1  12841  divgcdodd  12844  coprm  12845  coseq0q4123  15716  lgsquad2lem2  15972  umgrnloop0  16129  umgrislfupgrenlem  16142  lfgrnloopen  16145  3dom  16779  pwle2  16789  nninfalllem1  16803  nninfall  16804  nninfsellemqall  16810