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  1291  nalequcoms  1497  equidqe  1512  nnal  1629  ax6blem  1630  hbnt  1633  naecoms  1704  euor2  2064  moexexdc  2090  baroco  2113  necon3ai  2376  necon3bi  2377  nnral  2447  eueq3dc  2886  difin  3344  indifdir  3363  difrab  3381  csbprc  3439  ifandc  3541  nelpri  3584  nelprd  3586  opprc  3762  opprc1  3763  opprc2  3764  notnotsnex  4147  eldifpw  4435  nlimsucg  4523  nfvres  5498  nfunsn  5499  ressnop0  5645  ovprc  5850  ovprc1  5851  ovprc2  5852  mapprc  6590  ixpprc  6657  ixp0  6669  fiprc  6753  fidceq  6807  unfiexmid  6855  difinfsnlem  7033  3nsssucpw1  7154  onntri51  7158  onntri52  7162  fzdcel  9924  bcpasc  10622  flodddiv4lt  11808  bj-nnan  13271  bj-nnst  13290  nninfsellemsuc  13546