Theorem con1i 132

Description: A contraposition inference. Inference associated with con1 131. Its associated inference is mt3 183. (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.1	|- ( -. ph -> ps )

Assertion

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

Proof of Theorem con1i

Step	Hyp	Ref	Expression
1		id 23	. 2 |- ( -. ps -> -. ps )
2		con1i.1	. 2 |- ( -. ph -> ps )
3	1, 2	nsyl2 130	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:  pm2.24i  136  nsyl4  147  impi  151  simplim  154  pm3.13  503  nbior  868  pm5.55  905  rb-ax2  1632  rb-ax3  1633  rb-ax4  1634  spimfw  1787  hba1w  1866  sp  1912  axc4  1913  exmoeu  2300  moanim  2328  moexex  2341  necon3biOLD  2661  necon1aiOLD  2663  necon1bi  2664  fvrn0  5903  nfunsn  5912  mpt2xopxnop0  6969  ixpprc  7551  fineqv  7793  unbndrank  8312  pf1rcl  18872  wlkntrllem3  25136  stri  27745  hstri  27753  ddemeas  28898  hbntg  30239  bj-naecomsv  31098  hba1-o  32178  axc5c711  32198  naecoms-o  32207  axc5c4c711  36389  hbntal  36557