Theorem con3 94

Description: Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103.

Assertion

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

Proof of Theorem con3

Step	Hyp	Ref	Expression
1		negb 86	. . 3 |- (ps -> -. -. ps)
2	1	imim2i 17	. 2 |- ((ph -> ps) -> (ph -> -. -. ps))
3	2	con2d 91	1 |- ((ph -> ps) -> (-. ps -> -. ph))

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  con3d 95  impt 141  pm4.1 164  jao 340  mtt 711  pclem6 740  meredith 923  nicodraw 951  ax4 971  hbnt 1001  19.22 1038  ax11indn 1366  ralf0 2357  ivthlem7 7258  ivthlem7OLD 7267  hlimunii 9096

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

Copyright terms: Public domain