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  4255  exmid1stab  4304  nsuceq0g  4521  abnex  4550  reg2exmidlema  4638  ordsuc  4667  onnmin  4672  ssnel  4673  ordtri2or2exmid  4675  ontri2orexmidim  4676  reg3exmidlemwe  4683  acexmidlemab  6022  reldmtpos  6462  dmtpos  6465  2pwuninelg  6492  onunsnss  7152  snon0  7177  nninfisol  7392  exmidomni  7401  pr2ne  7457  ltexprlemdisj  7886  recexprlemdisj  7910  caucvgprlemnkj  7946  caucvgprprlemnkltj  7969  caucvgprprlemnkeqj  7970  caucvgprprlemnjltk  7971  inelr  8823  rimul  8824  recgt0  9089  zfz1iso  11168  isprm2  12769  nprmdvds1  12792  divgcdodd  12795  coprm  12796  coseq0q4123  15645  lgsquad2lem2  15901  umgrnloop0  16058  umgrislfupgrenlem  16071  lfgrnloopen  16074  3dom  16708  pwle2  16720  nninfalllem1  16734  nninfall  16735  nninfsellemqall  16741