Theorem mtod 107

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 719  mtbird 720  po2nr 2925  po3nr 2926  ordn2lp 2995  onssneli 3079  onsucuni2 3188  nlimsucg 3196  tfi 3207  nnlim 3231  peano5 3241  tz7.48-3 4259  oalimcl 4330  omlimcl 4345  oneo 4348  sdomnsym 4607  php3 4662  onomeneq 4665  rankr1 4820  rankel 4826  ondomcard 5007  alephordi 5024  cardaleph 5035  ltrpq 5239  prlem934 5293  suplem2pr 5316  zneo 6371  sqr2irrlem3 6927  abssubne0 7085  facndiv 7146  climrecl 7313  ivthlem6 7491  lmle 8171  nvex 8477  efif1lem5 9006  irredlem1 10599  mtand 11372  mtord 11373  ordtypelem6 11432  onsdom 11437  omsubdom 11443  elomsubsd 11446  infenomsub 11450  cptclsscpt 11489  alexsublem4 11499  filufint 11659  ufilen 11664  filcon 11665  rnelfmlem 11698  fmfnfm 11704  fcluscomp 11733  filnetlem3 11765  fsumlt1 11894

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

Copyright terms: Public domain