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  6930  fsetdmprc0  6954  ixpprc  7005  ixp0  7017  fiprc  7108  fidceq  7175  elssdc  7213  unfiexmid  7229  relprcnfsupp  7293  difinfsnlem  7445  3nsssucpw1  7601  onntri51  7605  onntri52  7609  indval0  9306  fzdcel  10461  bcpasc  11226  hashfibc  11305  hashf1lem2  11308  pfxclz  11473  flodddiv4lt  12730  prmdcz  12934  gsummptfidmsplit  14254  bj-nnan  16969  bj-imnimnn  16971  nnnotnotr  17221  wexmiddiffilem  17248  wexmiddifxylem  17250  nninfsellemsuc  17261