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  1319  nalequcoms  1527  equidqe  1542  nnal  1659  ax6blem  1660  hbnt  1663  naecoms  1734  euor2  2094  moexexdc  2120  baroco  2143  necon3ai  2406  necon3bi  2407  nnral  2477  eueq3dc  2923  difin  3384  indifdir  3403  difrab  3421  csbprc  3480  ifandc  3584  nelpri  3628  nelprd  3630  opprc  3811  opprc1  3812  opprc2  3813  notnotsnex  4199  eldifpw  4489  nlimsucg  4577  nfvres  5560  nfunsn  5561  ressnop0  5710  ovprc  5923  ovprc1  5924  ovprc2  5925  mapprc  6666  ixpprc  6733  ixp0  6745  fiprc  6829  fidceq  6883  unfiexmid  6931  difinfsnlem  7112  3nsssucpw1  7249  onntri51  7253  onntri52  7257  fzdcel  10054  bcpasc  10760  flodddiv4lt  11955  bj-nnan  14784  bj-imnimnn  14786  nnnotnotr  15038  nninfsellemsuc  15058