Theorem con1i 129

Description: A contraposition inference. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Mel L. 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 22	. 2 |- ( -. ps -> -. ps )
2		con1i.a	. 2 |- ( -. ph -> ps )
3	1, 2	nsyl2 127	1 |- ( -. ps -> ph )

Syntax hints:   -. wn 3   -> wi 4

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

This theorem is referenced by:  nsyl4  142  pm2.24i  144  impi  148  simplim  151  pm3.13  501  pm5.55  893  rb-ax2  1565  rb-ax3  1566  rb-ax4  1567  ax5e  1677  spimfw  1704  hba1w  1758  sp  1803  axc4  1804  hba1-o  2214  axc5c711  2234  naecoms-o  2243  exmoeu  2304  moanim  2345  moexex  2364  necon3biOLD  2690  necon1aiOLD  2692  necon1bi  2693  fvrn0  5879  nfunsn  5888  mpt2xopxnop0  6933  ixpprc  7480  fineqv  7725  unbndrank  8249  pf1rcl  18149  wlkntrllem3  24225  stri  26838  hstri  26846  ddemeas  27834  hbntg  28801  axc5c4c711  30841  hbntal  32281  bj-naecomsv  33274