Theorem necon1ai 2960

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 2958	. 2 ⊢ (𝐴 ≠ 𝐵 → ¬ ¬ 𝜑)
3	2	notnotrd 133	1 ⊢ (𝐴 ≠ 𝐵 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon1i  2966  opnz  5422  inisegn0  6058  iotan0  6483  tz6.12i  6861  fvfundmfvn0  6875  brfvopabrbr  6939  elfvmptrab1  6971  brovpreldm  8033  brovex  8166  brwitnlem  8436  cantnflem1  9604  carddomi2  9888  rankcf  10694  eliooxr  13351  iccssioo2  13366  elfzoel1  13605  elfzoel2  13606  ismnd  18699  lactghmga  19374  pmtrmvd  19425  mpfrcl  22076  mhpsclcl  22126  fsubbas  23845  filuni  23863  ptcmplem2  24031  itg1climres  25694  mbfi1fseqlem4  25698  dvferm1lem  25964  dvferm2lem  25966  dvferm  25968  dvivthlem1  25988  coeeq2  26220  coe1termlem  26236  isppw  27094  dchrelbasd  27219  lgsne0  27315  wlkvv  29713  eldm3  35962  brfvimex  44474  brovmptimex  44475  clsneibex  44550  neicvgbex  44560  iotan0aiotaex  47556  afvnufveq  47610  gricrcl  48405  grlicrcl  48498  grilcbri2  48502  fvconstr  49352  fvconstrn0  49353  fvconstr2  49354  discsubc  49554  oppfrcl  49618  oppfrcl2  49619  oppfrcl3  49620  eloppf  49623  eloppf2  49624  oppcup3  49699  oppc1stflem  49777  catcrcl  49885