Theorem mtod 653

Description: Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

Hypotheses

Ref	Expression
mtod.1	|- ( ph -> -. ch )
mtod.2	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
mtod	|- ( ph -> -. ps )

Proof of Theorem mtod

Step	Hyp	Ref	Expression
1		mtod.2	. 2 |- ( ph -> ( ps -> ch ) )
2		mtod.1	. . 3 |- ( ph -> -. ch )
3	2	a1d 22	. 2 |- ( ph -> ( ps -> -. ch ) )
4	1, 3	pm2.65d 650	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 604  ax-in2 605

This theorem is referenced by:  mtoi  654  mtand  655  mtbid  662  mtbird  663  pwntru  4130  po2nr  4239  po3nr  4240  sotricim  4253  elirr  4464  ordn2lp  4468  en2lp  4477  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  nndomo  6766  fnfi  6833  difinfsnlem  6992  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  caucvgprlemladdrl  7510  caucvgprprlemaddq  7540  msqge0  8402  mulge0  8405  squeeze0  8686  elnn0z  9091  fznlem  9852  frec2uzf1od  10210  facndiv  10517  sumrbdclem  11178  prodrbdclem  11372  alzdvds  11588  fzm1ndvds  11590  fzo0dvdseq  11591  rpdvds  11816  nonsq  11921  ennnfonelemim  11973  bldisj  12609  bj-nnen2lp  13323  pwtrufal  13365  refeq  13398