Theorem con3i 621

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 617	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 603  ax-in2 604

This theorem is referenced by:  notnotnot  623  conax1  642  pm5.21ni  692  pm2.45  727  pm2.46  728  pm3.14  742  3ianorr  1287  nalequcoms  1497  equidqe  1512  ax6blem  1628  hbnt  1631  naecoms  1702  euor2  2055  moexexdc  2081  baroco  2104  necon3ai  2355  necon3bi  2356  eueq3dc  2853  difin  3308  indifdir  3327  difrab  3345  csbprc  3403  ifandc  3503  nelpri  3546  nelprd  3548  opprc  3721  opprc1  3722  opprc2  3723  notnotsnex  4106  eldifpw  4393  nlimsucg  4476  nfvres  5447  nfunsn  5448  ressnop0  5594  ovprc  5799  ovprc1  5800  ovprc2  5801  mapprc  6539  ixpprc  6606  ixp0  6618  fiprc  6702  fidceq  6756  unfiexmid  6799  difinfsnlem  6977  fzdcel  9813  bcpasc  10505  flodddiv4lt  11622  bj-nnan  12937  bj-nnal  12938  bj-nnst  12953  nninfsellemsuc  13197