Theorem con3i 622

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  notnotnot  624  conax1  643  pm5.21ni  693  pm2.45  728  pm2.46  729  pm3.14  743  3ianorr  1299  nalequcoms  1505  equidqe  1520  nnal  1637  ax6blem  1638  hbnt  1641  naecoms  1712  euor2  2072  moexexdc  2098  baroco  2121  necon3ai  2385  necon3bi  2386  nnral  2456  eueq3dc  2900  difin  3359  indifdir  3378  difrab  3396  csbprc  3454  ifandc  3557  nelpri  3600  nelprd  3602  opprc  3779  opprc1  3780  opprc2  3781  notnotsnex  4166  eldifpw  4455  nlimsucg  4543  nfvres  5519  nfunsn  5520  ressnop0  5666  ovprc  5877  ovprc1  5878  ovprc2  5879  mapprc  6618  ixpprc  6685  ixp0  6697  fiprc  6781  fidceq  6835  unfiexmid  6883  difinfsnlem  7064  3nsssucpw1  7192  onntri51  7196  onntri52  7200  fzdcel  9975  bcpasc  10679  flodddiv4lt  11873  bj-nnan  13617  bj-imnimnn  13619  nnnotnotr  13872  nninfsellemsuc  13892