Theorem necon1ai 2952

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

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

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 2926

This theorem is referenced by:  necon1i  2958  opnz  5428  inisegn0  6058  iotan0  6489  tz6.12i  6868  fvfundmfvn0  6883  brfvopabrbr  6947  elfvmptrab1  6978  brovpreldm  8045  brovex  8178  brwitnlem  8448  cantnflem1  9618  carddomi2  9899  rankcf  10706  eliooxr  13341  iccssioo2  13356  elfzoel1  13594  elfzoel2  13595  ismnd  18640  lactghmga  19311  pmtrmvd  19362  mpfrcl  21968  mhpsclcl  22010  fsubbas  23730  filuni  23748  ptcmplem2  23916  itg1climres  25591  mbfi1fseqlem4  25595  dvferm1lem  25864  dvferm2lem  25866  dvferm  25868  dvivthlem1  25889  coeeq2  26123  coe1termlem  26139  isppw  27000  dchrelbasd  27126  lgsne0  27222  wlkvv  29530  eldm3  35721  brfvimex  43988  brovmptimex  43989  clsneibex  44064  neicvgbex  44074  iotan0aiotaex  47067  afvnufveq  47121  gricrcl  47887  grlicrcl  47972  grilcbri2  47976  fvconstr  48823  fvconstrn0  48824  fvconstr2  48825  discsubc  49026  oppfrcl  49090  oppfrcl2  49091  oppfrcl3  49092  eloppf  49095  eloppf2  49096  oppcup3  49171  oppc1stflem  49249  catcrcl  49357