Theorem con1i 123

Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 19-Jun-2013.)

Hypothesis

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

Assertion

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

Proof of Theorem con1i

Step	Hyp	Ref	Expression
1		id 20	. 2 |- ( -. ps -> -. ps )
2		con1i.a	. 2 |- ( -. ph -> ps )
3	1, 2	nsyl2 121	1 |- ( -. ps -> ph )

Syntax hints:   -. wn 3   -> wi 4

This theorem is referenced by:  nsyl4  136  pm2.24i  138  impi  142  simplim  145  pm3.13  488  pm5.55  868  rb-ax2  1524  rb-ax3  1525  rb-ax4  1526  ax17e  1625  spimfw  1653  hba1w  1718  sp  1759  ax5o  1761  hbntOLD  1796  hba1OLD  1801  nfndOLD  1806  hbimdOLD  1831  naecoms  2004  hba1-o  2199  ax467  2219  naecoms-o  2228  necon3bi  2608  necon1ai  2609  fvrn0  5712  nfunsn  5720  mpt2xopxnop0  6425  ixpprc  7042  fineqv  7283  unbndrank  7724  pf1rcl  19922  wlkntrllem3  21514  stri  23713  hstri  23721  hbntg  25376  ax4567  27469  hbntal  28351  naecomsNEW7  29320

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