Theorem mtod 108

Description: Modus tollens deduction.

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.1	. 2 |- (ph -> -. ch)
2		mtod.2	. . 3 |- (ph -> (ps -> ch))
3	2	con3d 95	. 2 |- (ph -> (-. ch -> -. ps))
4	1, 3	mpd 26	1 |- (ph -> -. ps)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  mtbid 714  mtbird 715  po2nr 2847  po3nr 2848  ordn2lp 2968  onsucuni2 3091  onssneli 3101  nlimsucg 3112  tfi 3126  nnlim 3144  peano5 3153  tz7.48-3 3958  oalimcl 4194  omlimcl 4209  oneo 4212  sdomnsym 4462  php3 4515  php3OLD 4516  onomeneq 4519  rankr1 4674  rankel 4680  ondomcard 4857  alephordi 4874  cardaleph 4885  ltrpq 5085  prlem934 5139  suplem2pr 5162  zneo 6200  sqr2irrlem3 6726  abssubne0t 6882  facndivt 6943  climrecl 7110  ivthlem6 7286  lmle 7960  nvex 8230  efif1lem5 8734  irredlem1 10317

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

Copyright terms: Public domain