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 971  19.8a 1025  a4ime 1156  sbn 1226  a4sbe 1238  a12study 1371  exists2 1451  necon2ai 1603  necon2bi 1604  eueq3 1910  psstr 2140  elndif 2154  n0i 2275  iununi 2606  zfpair 2767  opprc1b 2786  frirr 2914  onssneli 3091  dflim3 3108  onxpdisj 3231  funopg 3533  dfrdg2 3918  ixp0 4345  bren2 4370  domnsym 4443  rankr1 4646  aceq6b 4714  carden 4803  alephsucdom 4852  alephval3 4875  ltxrltt 5472  elnnz1 6102  bcthlem33 7965  issubg 8053  strlem1 10087  chrelat2 10200

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

Copyright terms: Public domain