Theorem con3i 641

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

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  notnotnot  643  nsyl5  659  conax1  663  pm5.21ni  715  pm2.45  750  pm2.46  751  pm3.14  765  3ianorr  1350  nalequcoms  1570  equidqe  1585  nnal  1702  hbn  1703  hbnt  1705  naecoms  1776  euor2  2145  moexexdc  2171  baroco  2194  necon3ai  2469  necon3bi  2470  nnral  2540  eueq3dc  3000  difin  3468  indifdir  3487  difrab  3507  csbprc  3572  ifandc  3681  nelpri  3733  nelprd  3735  opprc  3925  opprc1  3926  opprc2  3927  notnotsnex  4326  eldifpw  4625  nlimsucg  4715  nfvres  5735  nfunsn  5736  ressnop0  5899  ovprc  6124  ovprc1  6125  ovprc2  6126  mapprc  6931  fsetdmprc0  6955  ixpprc  7007  ixp0  7019  fiprc  7110  fidceq  7177  elssdc  7215  unfiexmid  7231  relprcnfsupp  7295  difinfsnlem  7445  3nsssucpw1  7601  onntri51  7605  onntri52  7609  indval0  9306  fzdcel  10460  bcpasc  11225  hashfibc  11304  hashf1lem2  11307  pfxclz  11472  flodddiv4lt  12729  prmdcz  12933  gsummptfidmsplit  14253  bj-nnan  16986  bj-imnimnn  16988  nnnotnotr  17238  wexmiddiffilem  17265  wexmiddifxylem  17267  nninfsellemsuc  17278