Theorem con2i 97

Description: A contraposition inference.

Hypothesis

Ref	Expression
con2.a	|- (ph -> -. ps)

Assertion

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

Proof of Theorem con2i

Step	Hyp	Ref	Expression
1		nega 84	. . 3 |- (-. -. ph -> ph)
2		con2.a	. . 3 |- (ph -> -. ps)
3	1, 2	syl 10	. 2 |- (-. -. ph -> -. ps)
4	3	a3i 74	1 |- (ps -> -. ph)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  mt2 109  nsyl3 119  con1bii 220  pm3.14 318  ax5o 972  19.8a 1027  a4ime 1158  sbn 1229  a4sbe 1241  a12study 1376  exists2 1456  necon2ai 1608  necon2bi 1609  eueq3 1915  psstr 2146  elndif 2160  n0i 2281  iununi 2611  zfpair 2772  opprc1b 2791  frirr 2919  onssneli 3096  dflim3 3113  onxpdisj 3236  funopg 3539  dfrdg2 3924  ixp0 4351  bren2 4376  domnsym 4449  rankr1 4654  aceq6b 4722  carden 4811  alephsucdom 4860  alephval3 4883  ltxrltt 5480  elnnz1 6110  bcthlem33 7981  issubg 8068  strlem1 10115  chrelat2 10229

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

Copyright terms: Public domain