Theorem con1i 129

Description: A contraposition inference. Its associated inference is mt3 180. (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  nbior  860  pm5.55  897  rb-ax2  1573  rb-ax3  1574  rb-ax4  1575  spimfw  1724  hba1w  1800  sp  1845  axc4  1846  hba1-o  2214  axc5c711  2234  naecoms-o  2243  exmoeu  2302  moanim  2336  moexex  2349  necon3biOLD  2673  necon1aiOLD  2675  necon1bi  2676  fvrn0  5878  nfunsn  5887  mpt2xopxnop0  6945  ixpprc  7492  fineqv  7737  unbndrank  8263  pf1rcl  18259  wlkntrllem3  24435  stri  27048  hstri  27056  ddemeas  28081  hbntg  29213  axc5c4c711  31262  hbntal  33059  bj-naecomsv  34066