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  4231  eldifpw  4524  nlimsucg  4614  nfvres  5610  nfunsn  5611  ressnop0  5765  ovprc  5980  ovprc1  5981  ovprc2  5982  mapprc  6739  ixpprc  6806  ixp0  6818  fiprc  6907  fidceq  6966  unfiexmid  7015  difinfsnlem  7201  3nsssucpw1  7348  onntri51  7352  onntri52  7356  fzdcel  10162  bcpasc  10911  flodddiv4lt  12249  bj-nnan  15676  bj-imnimnn  15678  nnnotnotr  15930  nninfsellemsuc  15953