Theorem con3i 604

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

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 586  ax-in2 587

This theorem is referenced by:  notnotnot  606  conax1  625  pm5.21ni  675  pm2.45  710  pm2.46  711  pm3.14  725  3ianorr  1270  nalequcoms  1480  equidqe  1495  ax6blem  1611  hbnt  1614  naecoms  1685  euor2  2033  moexexdc  2059  baroco  2082  necon3ai  2331  necon3bi  2332  eueq3dc  2827  difin  3279  indifdir  3298  difrab  3316  csbprc  3374  ifandc  3474  nelpri  3517  nelprd  3519  opprc  3692  opprc1  3693  opprc2  3694  notnotsnex  4071  eldifpw  4358  nlimsucg  4441  nfvres  5408  nfunsn  5409  ressnop0  5555  ovprc  5760  ovprc1  5761  ovprc2  5762  mapprc  6500  ixpprc  6567  ixp0  6579  fiprc  6663  fidceq  6716  unfiexmid  6759  difinfsnlem  6936  fzdcel  9713  bcpasc  10405  flodddiv4lt  11481  bj-nnan  12641  bj-nnal  12642  bj-nnst  12657  nninfsellemsuc  12900