Theorem mtoi 666

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 665	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 615  ax-in2 616

This theorem is referenced by:  mtbii  676  mtbiri  677  pwnss  4204  exmid1stab  4253  nsuceq0g  4466  abnex  4495  reg2exmidlema  4583  ordsuc  4612  onnmin  4617  ssnel  4618  ordtri2or2exmid  4620  ontri2orexmidim  4621  reg3exmidlemwe  4628  acexmidlemab  5940  reldmtpos  6341  dmtpos  6344  2pwuninelg  6371  onunsnss  7016  snon0  7039  nninfisol  7237  exmidomni  7246  pr2ne  7302  ltexprlemdisj  7721  recexprlemdisj  7745  caucvgprlemnkj  7781  caucvgprprlemnkltj  7804  caucvgprprlemnkeqj  7805  caucvgprprlemnjltk  7806  inelr  8659  rimul  8660  recgt0  8925  zfz1iso  10988  isprm2  12472  nprmdvds1  12495  divgcdodd  12498  coprm  12499  coseq0q4123  15339  lgsquad2lem2  15592  pwle2  15972  nninfalllem1  15982  nninfall  15983  nninfsellemqall  15989