Theorem con3i 594

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  pm2.51  613  pm5.21ni  651  notnotnot  660  pm2.45  689  pm2.46  690  pm3.14  702  3ianorr  1240  nalequcoms  1450  equidqe  1465  ax6blem  1580  hbnt  1583  naecoms  1652  euor2  1999  moexexdc  2025  baroco  2048  necon3ai  2294  necon3bi  2295  eueq3dc  2766  difin  3201  indifdir  3220  difrab  3238  csbprc  3289  nelpri  3422  opprc  3591  opprc1  3592  opprc2  3593  eldifpw  4226  nlimsucg  4309  nfvres  5227  nfunsn  5228  ressnop0  5365  ovprc  5560  ovprc1  5561  ovprc2  5562  fiprc  6315  fidceq  6354  fzdcel  9059  bcpasc  9693  flodddiv4lt  10336