Theorem con1i 134

Description: A contraposition inference. Inference associated with con1 133. Its associated inference is mt3 185. (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 22	. 2 |- ( -. ps -> -. ps )
2		con1i.1	. 2 |- ( -. ph -> ps )
3	1, 2	nsyl2 132	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  138  nsyl4  149  impi  153  simplim  156  pm3.13  508  nbior  876  pm5.55  913  rb-ax2  1647  rb-ax3  1648  rb-ax4  1649  spimfw  1806  hba1w  1894  sp  1948  axc4  1949  exmoeu  2342  moanim  2369  moexex  2381  necon1bi  2664  fvrn0  5910  nfunsn  5919  mpt2xneldm  6985  mpt2xopxnop0  6988  ixpprc  7569  fineqv  7813  unbndrank  8339  pf1rcl  18986  wlkntrllem3  25340  stri  27959  hstri  27967  ddemeas  29108  hbntg  30501  bj-naecomsv  31395  hba1-o  32514  axc5c711  32534  naecoms-o  32543  axc5c4c711  36796  hbntal  36964