Theorem necon3ai 2951

Description: Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 28-Oct-2024.)

Hypothesis

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

Assertion

Ref	Expression
necon3ai	⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)

Proof of Theorem necon3ai

Step	Hyp	Ref	Expression
1		neneq 2932	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
2		necon3ai.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	nsyl 140	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-ne 2927

This theorem is referenced by:  necon1ai  2953  necon3i  2958  neneor  3026  nelsn  4633  disjsn2  4679  prnesn  4827  opelopabsb  5493  funsndifnop  7126  ord1eln01  8463  map0b  8859  mapdom3  9119  cflim2  10223  isfin4p1  10275  fpwwe2lem12  10602  tskuni  10743  recextlem2  11816  hashprg  14367  eqsqrt2d  15342  gcd1  16505  gcdzeq  16529  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  phimullem  16756  pcgcd1  16855  pc2dvds  16857  pockthlem  16883  ablfacrplem  20004  znrrg  21482  opnfbas  23736  supfil  23789  itg1addlem4  25607  itg1addlem5  25608  mpodvdsmulf1o  27111  dvdsmulf1o  27113  ppiub  27122  dchrelbas4  27161  2sqlem8  27344  tgldimor  28436  subfacp1lem6  35179  cvmsss2  35268  ax6e2ndeq  44556  supminfxr2  45472  fourierdlem56  46167  ichnreuop  47477