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 974  19.8a 1029  a4ime 1160  sbn 1231  a4sbe 1243  a12study 1378  exists2 1458  necon2ai 1611  necon2bi 1612  eueq3 1919  psstr 2150  elndif 2164  n0i 2285  iununi 2616  zfpair 2777  opprc1b 2796  frirr 2924  onssneli 3101  dflim3 3118  onxpdisj 3241  funopg 3547  dfrdg2 3933  ixp0 4361  bren2 4389  domnsym 4463  rankr1 4674  aceq6b 4742  carden 4831  alephsucdom 4880  alephval3 4903  ltxrltt 5500  elnnz1 6155  bcthlem33 8031  issubg 8116  strlem1 10177  chrelat2 10292  top2ind 10548

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

Copyright terms: Public domain