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	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
con3i	⊢ (¬ 𝜓 → ¬ 𝜑)

Proof of Theorem con3i

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
2		con3i.a	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	nsyl 637	1 ⊢ (¬ 𝜓 → ¬ 𝜑)

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  7440  3nsssucpw1  7596  onntri51  7600  onntri52  7604  indval0  9300  fzdcel  10455  bcpasc  11220  hashfibc  11299  hashf1lem2  11302  pfxclz  11467  flodddiv4lt  12724  prmdcz  12928  bj-nnan  16930  bj-imnimnn  16932  nnnotnotr  17182  wexmiddiffilem  17209  wexmiddifxylem  17211  nninfsellemsuc  17221