Theorem con3 110

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		notnot1 102	. . 3 |- (ps -> -. -. ps)
2	1	imim2i 11	. 2 |- ((ph -> ps) -> (ph -> -. -. ps))
3	2	con2d 107	1 |- ((ph -> ps) -> (-. ps -> -. ph))

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  con3d 111  impt 158  con34b 183  jao 367  mtt 780  pclem6 813  meredithOLD 1201  nic-ax 1239  nic-axALT 1240  hbnt 1349  exim 1386  ax11indn 1757  rexim 2194  ralf0 2975  tratrb 5831  ivthlem7 8549  hlimuniii 10741  bnj9 12372  bnj9OLD 12373  bnj10 12374  dfon2lem9 13857  hbntg 13872  naim1 14134  naim2 14135  lukshef-ax2 14239  fcluscf 15612  tratrbVD 16685  cvrexchlem 17059  cvratlem 17061

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

Copyright terms: Public domain