Theorem con1i 144

Description: A contraposition inference. Inference associated with con1 143. Its associated inference is mt3 192. (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 142	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  146  nsyl4  156  impi  160  simplim  163  pm3.13  522  nbior  905  pm5.55  939  rb-ax2  1678  rb-ax3  1679  rb-ax4  1680  spimfw  1878  hba1w  1974  hba1wOLD  1975  hbe1a  2022  sp  2053  axc4  2130  exmoeu  2502  moanim  2529  moexex  2541  necon1bi  2822  fvrn0  6216  nfunsn  6225  mpt2xneldm  7338  mpt2xopxnop0  7341  ixpprc  7929  fineqv  8175  unbndrank  8705  pf1rcl  19713  stri  29116  hstri  29124  ddemeas  30299  hbntg  31711  bj-modalb  32706  hba1-o  34182  axc5c711  34203  naecoms-o  34212  axc5c4c711  38602  hbntal  38769