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 1365  ralf0 2356  ivthlem7 7239  ivthlem7OLD 7248  hlimunii 9063

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

Copyright terms: Public domain