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  1541  equidqe  1556  nnal  1673  ax6blem  1674  hbnt  1677  naecoms  1748  euor2  2114  moexexdc  2140  baroco  2163  necon3ai  2427  necon3bi  2428  nnral  2498  eueq3dc  2954  difin  3418  indifdir  3437  difrab  3455  csbprc  3514  ifandc  3620  nelpri  3667  nelprd  3669  opprc  3854  opprc1  3855  opprc2  3856  notnotsnex  4247  eldifpw  4542  nlimsucg  4632  nfvres  5633  nfunsn  5634  ressnop0  5788  ovprc  6003  ovprc1  6004  ovprc2  6005  mapprc  6762  ixpprc  6829  ixp0  6841  fiprc  6931  fidceq  6992  unfiexmid  7041  difinfsnlem  7227  3nsssucpw1  7382  onntri51  7386  onntri52  7390  fzdcel  10197  bcpasc  10948  pfxclz  11170  flodddiv4lt  12364  bj-nnan  15872  bj-imnimnn  15874  nnnotnotr  16125  nninfsellemsuc  16151