Theorem con2i 113

Description: A contraposition inference. (The proof was shortened by O'Cat, 28-Nov-2008.)

Hypothesis

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

Assertion

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

Proof of Theorem con2i

Step	Hyp	Ref	Expression
1		con2.a	. 2 |- (ph -> -. ps)
2		con2 106	. 2 |- ((ph -> -. ps) -> (ps -> -. ph))
3	1, 2	ax-mp 7	1 |- (ps -> -. ph)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  mt2 124  nsyl3 134  con1bii 237  pm3.14 345  consensus 844  ax5o 1320  19.8a 1376  a4ime 1521  sbn 1601  a4sbe 1613  a12study 1769  exists2OLD 1864  necon3ai 2043  necon2aiOLD 2052  necon2bi 2053  necon4ai 2067  eueq3 2430  ssnpss 2712  psstr 2714  elndif 2732  n0i 2880  iununi 3331  iununiOLD 3332  zfpair 3522  opprc1b 3542  frirr 3634  onssneli 3779  nlimsucg 3923  dflim3OLD 3931  onxpdisj 4068  onxpdisjOLD 4069  funopg 4454  dfrdg2 5141  ixp0 5420  bren2 5448  domnsym 5526  rankr1 5785  aceq6b 5904  carden 5981  alephsucdom 6028  alephval3 6051  ltxrlt 6669  renfdisj 6712  elnnz1 7364  bcthlem33 9309  issubg 9425  strlem1 11822  chrelat2i 11937  intn3an1d 14263  intn3an2d 14264  intn3an3d 14265  top2ind 14897  finminlem 15367  ipo0 16426  ifr0 16427  hlrelat2 17052

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

Copyright terms: Public domain