Theorem con3i 595

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 591	1 |- ( -. ps -> -. ph )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 577  ax-in2 578

This theorem is referenced by:  pm2.51  614  pm5.21ni  652  notnotnot  661  pm2.45  690  pm2.46  691  pm3.14  703  3ianorr  1241  nalequcoms  1451  equidqe  1466  ax6blem  1581  hbnt  1584  naecoms  1653  euor2  2000  moexexdc  2026  baroco  2049  necon3ai  2295  necon3bi  2296  eueq3dc  2767  difin  3208  indifdir  3227  difrab  3245  csbprc  3296  nelpri  3430  opprc  3599  opprc1  3600  opprc2  3601  eldifpw  4234  nlimsucg  4317  nfvres  5238  nfunsn  5239  ressnop0  5376  ovprc  5571  ovprc1  5572  ovprc2  5573  fiprc  6360  fidceq  6404  unfiexmid  6438  fzdcel  9135  bcpasc  9790  flodddiv4lt  10480