Theorem necon3bd 2443

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 634	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝐴 = 𝐵))
3		df-ne 2401	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
4	2, 3	imbitrrdi 162	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1395   ≠ wne 2400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618

This theorem depends on definitions:  df-bi 117  df-ne 2401

This theorem is referenced by:  nelne1  2490  nelne2  2491  nssne1  3282  nssne2  3283  disjne  3545  difsn  3804  nbrne1  4101  nbrne2  4102  ac6sfi  7048  indpi  7517  zneo  9536  pc2dvds  12839  pcadd  12849  oddprmdvds  12863  4sqlem11  12910  isnzr2  14133  lssvneln0  14322  lgsne0  15702  lgsquadlem2  15742  lgsquadlem3  15743