Theorem mtod 95

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 87	. 2 |- (ph -> (-. ch -> -. ps))
4	1, 3	mpd 46	1 |- (ph -> -. ps)

Syntax hints:  -. wn 1   -> wi 2

This theorem is referenced by:  mtbid 536  mtbird 537  po2nr 2135  po3nr 2136  ordn2lp 2219  tfi 2244  onssneli 2349  nlimsuc 2363  nnlim 2385  peano5 2394  tz7.48-3 2996  oalimcl 3162  sdomnsym 3364  php3 3411  onomeneq 3414  rankr1 3518  rankel 3524  ondomcard 3663  alephordi 3679  cardaleph 3690  nlt1pi 3827  ltrpq 3879  prlem934 3933  suplem2pr 3956  zneo 4601  sqr2irrlem3 4779  hatomistic 5755

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

metamath.org