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  4324  eldifpw  4623  nlimsucg  4713  nfvres  5732  nfunsn  5733  ressnop0  5896  ovprc  6121  ovprc1  6122  ovprc2  6123  mapprc  6926  fsetdmprc0  6950  ixpprc  7001  ixp0  7013  fiprc  7104  fidceq  7171  elssdc  7209  unfiexmid  7225  relprcnfsupp  7288  difinfsnlem  7439  3nsssucpw1  7595  onntri51  7599  onntri52  7603  indval0  9297  fzdcel  10444  bcpasc  11204  hashfibc  11283  hashf1lem2  11286  pfxclz  11451  flodddiv4lt  12705  bj-nnan  16764  bj-imnimnn  16766  nnnotnotr  17016  wexmiddiffilem  17043  wexmiddifxylem  17045  nninfsellemsuc  17055