Theorem necon3ai 2965

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 2946	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵)
2		necon3ai.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	nsyl 140	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑)

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

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 2941

This theorem is referenced by:  necon1ai  2968  necon3i  2973  neneor  3042  nelsn  4666  disjsn2  4712  prnesn  4860  opelopabsb  5535  funsndifnop  7171  ord1eln01  8534  map0b  8923  mapdom3  9189  cflim2  10303  isfin4p1  10355  fpwwe2lem12  10682  tskuni  10823  recextlem2  11894  hashprg  14434  eqsqrt2d  15407  gcd1  16565  gcdzeq  16589  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  phimullem  16816  pcgcd1  16915  pc2dvds  16917  pockthlem  16943  ablfacrplem  20085  znrrg  21584  opnfbas  23850  supfil  23903  itg1addlem4  25734  itg1addlem5  25735  mpodvdsmulf1o  27237  dvdsmulf1o  27239  ppiub  27248  dchrelbas4  27287  2sqlem8  27470  tgldimor  28510  subfacp1lem6  35190  cvmsss2  35279  ax6e2ndeq  44579  supminfxr2  45480  fourierdlem56  46177  ichnreuop  47459