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 709  pclem6 738  meredith 920  nicodraw 948  hbnt 978  19.22 1015  ax11indn 1343  ralf0 2330  ivthlem7 7173  ivthlem7OLD 7182  hlimunii 9259

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

Copyright terms: Public domain