Theorem necon3bd 2463

Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)

Hypothesis

Ref	Expression
necon3bd.1	⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))

Assertion

Ref	Expression
necon3bd	⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

Proof of Theorem necon3bd

Step	Hyp	Ref	Expression
1		necon3bd.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
2	1	con3d 640	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝐴 = 𝐵))
3		df-ne 2421	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
4	2, 3	imbitrrdi 162	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1402   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  nelne1  2510  nelne2  2511  nssne1  3306  nssne2  3307  disjne  3578  difsn  3852  nbrne1  4149  nbrne2  4150  ac6sfi  7202  indpi  7709  zneo  9749  pc2dvds  13111  pcadd  13121  oddprmdvds  13135  4sqlem11  13182  isnzr2  14493  lssvneln0  14712  pellexlem1  16097  lgsne0  16169  lgsquadlem2  16209  lgsquadlem3  16210