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  499  nbior  858  pm5.55  895  rb-ax2  1593  rb-ax3  1594  rb-ax4  1595  spimfw  1745  hba1w  1822  sp  1867  axc4  1868  exmoeu  2252  moanim  2281  moexex  2294  necon3biOLD  2612  necon1aiOLD  2614  necon1bi  2615  fvrn0  5796  nfunsn  5805  mpt2xopxnop0  6861  ixpprc  7409  fineqv  7651  unbndrank  8173  pf1rcl  18498  wlkntrllem3  24684  stri  27292  hstri  27300  ddemeas  28364  hbntg  29403  axc5c4c711  31476  hbntal  33666  bj-naecomsv  34665  hba1-o  35041  axc5c711  35061  naecoms-o  35070