Theorem con3i 633

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 629	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 615  ax-in2 616

This theorem is referenced by:  notnotnot  635  nsyl5  651  conax1  655  pm5.21ni  705  pm2.45  740  pm2.46  741  pm3.14  755  3ianorr  1322  nalequcoms  1540  equidqe  1555  nnal  1672  ax6blem  1673  hbnt  1676  naecoms  1747  euor2  2112  moexexdc  2138  baroco  2161  necon3ai  2425  necon3bi  2426  nnral  2496  eueq3dc  2947  difin  3410  indifdir  3429  difrab  3447  csbprc  3506  ifandc  3610  nelpri  3657  nelprd  3659  opprc  3840  opprc1  3841  opprc2  3842  notnotsnex  4232  eldifpw  4525  nlimsucg  4615  nfvres  5612  nfunsn  5613  ressnop0  5767  ovprc  5982  ovprc1  5983  ovprc2  5984  mapprc  6741  ixpprc  6808  ixp0  6820  fiprc  6909  fidceq  6968  unfiexmid  7017  difinfsnlem  7203  3nsssucpw1  7350  onntri51  7354  onntri52  7358  fzdcel  10164  bcpasc  10913  flodddiv4lt  12282  bj-nnan  15709  bj-imnimnn  15711  nnnotnotr  15963  nninfsellemsuc  15986