Theorem mt2 109

Description: A rule similar to modus tollens.

Hypotheses

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

Assertion

Ref	Expression
mt2	|- -. ph

Proof of Theorem mt2

Step	Hyp	Ref	Expression
1		mt2.1	. 2 |- ps
2		mt2.2	. . 3 |- (ph -> -. ps)
3	2	con2i 97	. 2 |- (ps -> -. ph)
4	1, 3	ax-mp 7	1 |- -. ph

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  bijust 145  npss0 2299  tz7.49 3944  elirrv 4570  omelon 4601  cardom 4797  renfdisj 5512  sqrlem14 6616  sqrlem21 6623  sqrlem22 6624  climunii 7035  vcex 8137  hlimunii 9029  strlem1 10087

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

Copyright terms: Public domain