Theorem mt2 96

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

Syntax hints:  -. wn 1   -> wi 2

This theorem is referenced by:  bijust 126  npss0 1731  nlim0 2282  tz7.49 2997  eirrv 3449  omelon 3476  cardom 3632  0npi 3804  0npr 3890  sqrlem14 4744  sqrlem21 4751  sqrlem22 4752  climunii 4883  hlimunii 5143  strlem1 5691

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

metamath.org