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 713  mtbird 714  po2nr 2842  po3nr 2843  ordn2lp 2963  onsucuni2 3086  onssneli 3096  nlimsucg 3107  tfi 3121  nnlim 3139  peano5 3148  tz7.48-3 3949  oalimcl 4184  omlimcl 4199  oneo 4202  sdomnsym 4448  php3 4501  onomeneq 4504  rankr1 4654  rankel 4660  ondomcard 4837  alephordi 4854  cardaleph 4865  ltrpq 5065  prlem934 5119  suplem2pr 5142  zneo 6155  zneoOLD 6156  sqr2irrlem3 6664  abssubne0t 6828  facndivt 6888  climrecl 7055  ivthlem6 7229  ivthlem6OLD 7238  lmle 7911  nvex 8182  efif1lem5 8668  irredlem1 10254

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

Copyright terms: Public domain