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 716  mtbird 717  po2nr 2853  po3nr 2854  ordn2lp 2974  onsucuni2 3097  onssneli 3107  nlimsucg 3118  tfi 3132  nnlim 3150  peano5 3159  tz7.48-3 3964  oalimcl 4200  omlimcl 4215  oneo 4218  sdomnsym 4468  php3 4521  php3OLD 4522  onomeneq 4525  rankr1 4684  rankel 4690  ondomcard 4868  alephordi 4885  cardaleph 4896  ltrpq 5097  prlem934 5151  suplem2pr 5174  zneo 6202  sqr2irrlem3 6727  abssubne0t 6882  facndivt 6943  climrecl 7110  ivthlem6 7286  lmle 7957  nvex 8226  efif1lem5 8729  irredlem1 10312

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

Copyright terms: Public domain