Theorem mt2 123

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 112	. 2 |- (ps -> -. ph)
4	1, 3	ax-mp 7	1 |- -. ph

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  bijust 161  npss0OLD 2736  tz7.49 4979  elirrv 5510  omelon 5545  cardom 5668  renfdisjOLD 6509  sqrlem14 7731  sqrlem21 7738  sqrlem22 7739  climunii 8153  vcex 9326  hlimuniii 10533  strlem1 11614  nalf 13883  heiborlem40 15676

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

Copyright terms: Public domain