Theorem con3i 621

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotnot  623  conax1  642  pm5.21ni  692  pm2.45  727  pm2.46  728  pm3.14  742  3ianorr  1287  nalequcoms  1497  equidqe  1512  ax6blem  1628  hbnt  1631  naecoms  1702  euor2  2057  moexexdc  2083  baroco  2106  necon3ai  2357  necon3bi  2358  eueq3dc  2858  difin  3313  indifdir  3332  difrab  3350  csbprc  3408  ifandc  3508  nelpri  3551  nelprd  3553  opprc  3726  opprc1  3727  opprc2  3728  notnotsnex  4111  eldifpw  4398  nlimsucg  4481  nfvres  5454  nfunsn  5455  ressnop0  5601  ovprc  5806  ovprc1  5807  ovprc2  5808  mapprc  6546  ixpprc  6613  ixp0  6625  fiprc  6709  fidceq  6763  unfiexmid  6806  difinfsnlem  6984  fzdcel  9820  bcpasc  10512  flodddiv4lt  11633  bj-nnan  12948  bj-nnal  12949  bj-nnst  12964  nninfsellemsuc  13208