Theorem con3i 633

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotnot  635  nsyl5  651  conax1  655  pm5.21ni  705  pm2.45  740  pm2.46  741  pm3.14  755  3ianorr  1322  nalequcoms  1541  equidqe  1556  nnal  1673  ax6blem  1674  hbnt  1677  naecoms  1748  euor2  2113  moexexdc  2139  baroco  2162  necon3ai  2426  necon3bi  2427  nnral  2497  eueq3dc  2951  difin  3414  indifdir  3433  difrab  3451  csbprc  3510  ifandc  3615  nelpri  3662  nelprd  3664  opprc  3846  opprc1  3847  opprc2  3848  notnotsnex  4239  eldifpw  4532  nlimsucg  4622  nfvres  5623  nfunsn  5624  ressnop0  5778  ovprc  5993  ovprc1  5994  ovprc2  5995  mapprc  6752  ixpprc  6819  ixp0  6831  fiprc  6921  fidceq  6981  unfiexmid  7030  difinfsnlem  7216  3nsssucpw1  7367  onntri51  7371  onntri52  7375  fzdcel  10182  bcpasc  10933  pfxclz  11155  flodddiv4lt  12324  bj-nnan  15811  bj-imnimnn  15813  nnnotnotr  16064  nninfsellemsuc  16090