Theorem con3i 632

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotnot  634  conax1  653  pm5.21ni  703  pm2.45  738  pm2.46  739  pm3.14  753  3ianorr  1309  nalequcoms  1515  equidqe  1530  nnal  1647  ax6blem  1648  hbnt  1651  naecoms  1722  euor2  2082  moexexdc  2108  baroco  2131  necon3ai  2394  necon3bi  2395  nnral  2465  eueq3dc  2909  difin  3370  indifdir  3389  difrab  3407  csbprc  3466  ifandc  3569  nelpri  3613  nelprd  3615  opprc  3795  opprc1  3796  opprc2  3797  notnotsnex  4182  eldifpw  4471  nlimsucg  4559  nfvres  5540  nfunsn  5541  ressnop0  5689  ovprc  5900  ovprc1  5901  ovprc2  5902  mapprc  6642  ixpprc  6709  ixp0  6721  fiprc  6805  fidceq  6859  unfiexmid  6907  difinfsnlem  7088  3nsssucpw1  7225  onntri51  7229  onntri52  7233  fzdcel  10008  bcpasc  10712  flodddiv4lt  11906  bj-nnan  14028  bj-imnimnn  14030  nnnotnotr  14282  nninfsellemsuc  14302