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  5419  inisegn0  6055  iotan0  6480  tz6.12i  6858  fvfundmfvn0  6872  brfvopabrbr  6936  elfvmptrab1  6968  brovpreldm  8030  brovex  8163  brwitnlem  8433  cantnflem1  9599  carddomi2  9883  rankcf  10689  eliooxr  13321  iccssioo2  13336  elfzoel1  13574  elfzoel2  13575  ismnd  18663  lactghmga  19338  pmtrmvd  19389  mpfrcl  22041  mhpsclcl  22091  fsubbas  23810  filuni  23828  ptcmplem2  23996  itg1climres  25659  mbfi1fseqlem4  25663  dvferm1lem  25929  dvferm2lem  25931  dvferm  25933  dvivthlem1  25954  coeeq2  26188  coe1termlem  26204  isppw  27064  dchrelbasd  27190  lgsne0  27286  wlkvv  29684  eldm3  35949  brfvimex  44456  brovmptimex  44457  clsneibex  44532  neicvgbex  44542  iotan0aiotaex  47527  afvnufveq  47581  gricrcl  48348  grlicrcl  48441  grilcbri2  48445  fvconstr  49295  fvconstrn0  49296  fvconstr2  49297  discsubc  49497  oppfrcl  49561  oppfrcl2  49562  oppfrcl3  49563  eloppf  49566  eloppf2  49567  oppcup3  49642  oppc1stflem  49720  catcrcl  49828