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 714  pclem6 743  meredith 926  nicodraw 954  ax4 974  hbnt 1004  19.22 1041  ax11indn 1368  ralf0 2364  ivthlem7 7294  hlimunii 9110

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

Copyright terms: Public domain