Theorem con1i 111

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

Hypothesis

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

Assertion

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

Proof of Theorem con1i

Step	Hyp	Ref	Expression
1		con1.a	. 2 |- (-. ph -> ps)
2		con1 107	. 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:  con3i 113  pm2.24i 118  mt3 126  nsyl2 132  nsyl4 134  pm3.26im 153  pm3.27im 154  con1bii 236  pm3.13 342  pm5.15 726  meredith 1047  ax5o 1158  hbnt 1187  ax467 1208  nalequcoms 1342  necon3bi 1880  necon1ai 1882  necon1biOLD 1884  nfunsn 4517  unbndrank 5603  stri 11621  hstri 11629  hbntg 13663  rb-ax2 13950  rb-ax3 13951  rb-ax4 13952  ax4567 16041

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

Copyright terms: Public domain