Theorem necon1ai 2966

Description: Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)

Hypothesis

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

Assertion

Ref	Expression
necon1ai	⊢ (𝐴 ≠ 𝐵 → 𝜑)

Proof of Theorem necon1ai

Step	Hyp	Ref	Expression
1		necon1ai.1	. . 3 ⊢ (¬ 𝜑 → 𝐴 = 𝐵)
2	1	necon3ai 2963	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ ¬ 𝜑)
3	2	notnotrd 133	1 ⊢ (𝐴 ≠ 𝐵 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2938

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 2939

This theorem is referenced by:  necon1i  2972  opnz  5484  inisegn0  6119  iotan0  6553  tz6.12i  6935  fvfundmfvn0  6950  brfvopabrbr  7013  elfvmptrab1  7044  brovpreldm  8113  brovex  8246  brwitnlem  8544  cantnflem1  9727  carddomi2  10008  rankcf  10815  1re  11259  eliooxr  13442  iccssioo2  13457  elfzoel1  13694  elfzoel2  13695  ismnd  18763  lactghmga  19438  pmtrmvd  19489  mpfrcl  22127  mhpsclcl  22169  fsubbas  23891  filuni  23909  ptcmplem2  24077  itg1climres  25764  mbfi1fseqlem4  25768  dvferm1lem  26037  dvferm2lem  26039  dvferm  26041  dvivthlem1  26062  coeeq2  26296  coe1termlem  26312  isppw  27172  dchrelbasd  27298  lgsne0  27394  wlkvv  29660  eldm3  35741  brfvimex  44016  brovmptimex  44017  clsneibex  44092  neicvgbex  44102  iotan0aiotaex  47043  afvnufveq  47097  gricrcl  47821  grlicrcl  47903  grilcbri2  47907  fvconstr  48686  fvconstrn0  48687  fvconstr2  48688