Theorem con3i 635

Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)

Hypothesis

Ref	Expression
con3i.a	|- ( ph -> ps )

Assertion

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

Proof of Theorem con3i

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( -. ps -> -. ps )
2		con3i.a	. 2 |- ( ph -> ps )
3	1, 2	nsyl 631	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-in1 617  ax-in2 618

This theorem is referenced by:  notnotnot  637  nsyl5  653  conax1  657  pm5.21ni  708  pm2.45  743  pm2.46  744  pm3.14  758  3ianorr  1343  nalequcoms  1563  equidqe  1578  nnal  1695  ax6blem  1696  hbnt  1699  naecoms  1770  euor2  2136  moexexdc  2162  baroco  2185  necon3ai  2449  necon3bi  2450  nnral  2520  eueq3dc  2977  difin  3441  indifdir  3460  difrab  3478  csbprc  3537  ifandc  3643  nelpri  3690  nelprd  3692  opprc  3878  opprc1  3879  opprc2  3880  notnotsnex  4271  eldifpw  4568  nlimsucg  4658  nfvres  5663  nfunsn  5664  ressnop0  5820  ovprc  6037  ovprc1  6038  ovprc2  6039  mapprc  6799  ixpprc  6866  ixp0  6878  fiprc  6968  fidceq  7031  unfiexmid  7080  difinfsnlem  7266  3nsssucpw1  7421  onntri51  7425  onntri52  7429  fzdcel  10236  bcpasc  10988  pfxclz  11211  flodddiv4lt  12449  bj-nnan  16100  bj-imnimnn  16102  nnnotnotr  16353  nninfsellemsuc  16378