Theorem con3i 632

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 628	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 614  ax-in2 615

This theorem is referenced by:  notnotnot  634  conax1  653  pm5.21ni  703  pm2.45  738  pm2.46  739  pm3.14  753  3ianorr  1309  nalequcoms  1517  equidqe  1532  nnal  1649  ax6blem  1650  hbnt  1653  naecoms  1724  euor2  2084  moexexdc  2110  baroco  2133  necon3ai  2396  necon3bi  2397  nnral  2467  eueq3dc  2913  difin  3374  indifdir  3393  difrab  3411  csbprc  3470  ifandc  3574  nelpri  3618  nelprd  3620  opprc  3801  opprc1  3802  opprc2  3803  notnotsnex  4189  eldifpw  4479  nlimsucg  4567  nfvres  5550  nfunsn  5551  ressnop0  5699  ovprc  5912  ovprc1  5913  ovprc2  5914  mapprc  6654  ixpprc  6721  ixp0  6733  fiprc  6817  fidceq  6871  unfiexmid  6919  difinfsnlem  7100  3nsssucpw1  7237  onntri51  7241  onntri52  7245  fzdcel  10042  bcpasc  10748  flodddiv4lt  11943  bj-nnan  14527  bj-imnimnn  14529  nnnotnotr  14781  nninfsellemsuc  14800