Theorem mtoi 107

Description: Modus tollens inference.

Hypotheses

Ref	Expression
mtoi.1	|- -. ch
mtoi.2	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
mtoi	|- (ph -> -. ps)

Proof of Theorem mtoi

Step	Hyp	Ref	Expression
1		mtoi.1	. 2 |- -. ch
2		mtoi.2	. . 3 |- (ph -> (ps -> ch))
3	2	con3d 95	. 2 |- (ph -> (-. ch -> -. ps))
4	1, 3	mpi 44	1 |- (ph -> -. ps)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  mtbii 720  mtbiri 721  exists2 1465  nsuceq0 3067  onssneli2 3116  unixp0 3532  funopg 3561  tz7.48-3 3972  tz7.49 3973  abianfp 3976  pwuninel 4501  2pwuninel 4502  ssrankr1 4688  rankxplim3 4726  zorn2lem4 4803  zorn2lem7 4806  carduni 4871  alephle 4897  alephfp 4913  nd1 4951  nd2 4952  axunnd 4961  nnunb 6076  indstr 6411  climunii 7112  efne0t 7383  infdif 7583  hlimunii 9115  hon0 9726  fiiu 10457  fiiu2 10492

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

Copyright terms: Public domain