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  conax1  654  pm5.21ni  704  pm2.45  739  pm2.46  740  pm3.14  754  3ianorr  1320  nalequcoms  1528  equidqe  1543  nnal  1660  ax6blem  1661  hbnt  1664  naecoms  1735  euor2  2100  moexexdc  2126  baroco  2149  necon3ai  2413  necon3bi  2414  nnral  2484  eueq3dc  2934  difin  3396  indifdir  3415  difrab  3433  csbprc  3492  ifandc  3595  nelpri  3642  nelprd  3644  opprc  3825  opprc1  3826  opprc2  3827  notnotsnex  4216  eldifpw  4508  nlimsucg  4598  nfvres  5588  nfunsn  5589  ressnop0  5739  ovprc  5953  ovprc1  5954  ovprc2  5955  mapprc  6706  ixpprc  6773  ixp0  6785  fiprc  6869  fidceq  6925  unfiexmid  6974  difinfsnlem  7158  3nsssucpw1  7296  onntri51  7300  onntri52  7304  fzdcel  10106  bcpasc  10837  flodddiv4lt  12077  bj-nnan  15228  bj-imnimnn  15230  nnnotnotr  15482  nninfsellemsuc  15502