Theorem con2i 89

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 78	. . 3 |- (-. -. ph -> ph)
2		con2.a	. . 3 |- (ph -> -. ps)
3	1, 2	syl 12	. 2 |- (-. -. ph -> -. ps)
4	3	a3i 69	1 |- (ps -> -. ph)

Syntax hints:  -. wn 1   -> wi 2

This theorem is referenced by:  mt2 96  nsyl3 104  bicon1i 193  19.8a 712  a4c 843  sbn1 880  sbea4 894  exists2 1073  cla4ev 1401  eueq3 1430  psstr 1574  elndif 1593  n0i 1712  minel 1743  zfpair 1891  opprc1b 1906  intex 1986  iununi 2037  frirr 2176  0ellim 2285  onssneli 2349  dflim3 2368  onxpdisj 2476  map0 3268  bren2 3293  domnsym 3365  inf3lem3 3466  rankr1 3518  aceq6b 3565  kmlem6 3585  carden 3638  alephsucdom 3685  nnne0t 4444  elnnz1 4581  strlem1 5691  chrelat2 5758

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

metamath.org