Theorem necon1ai 2961

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2934

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 208  df-ne 2935

This theorem is referenced by:  necon1i  2967  opnz  5413  inisegn0  6050  iotan0  6475  tz6.12i  6853  fvfundmfvn0  6867  brfvopabrbr  6932  elfvmptrab1  6964  brovpreldm  8028  brovex  8162  brwitnlem  8432  cantnflem1  9601  carddomi2  9885  rankcf  10691  eliooxr  13348  iccssioo2  13363  elfzoel1  13602  elfzoel2  13603  ismnd  18696  lactghmga  19371  pmtrmvd  19422  mpfrcl  22061  mhpsclcl  22135  fsubbas  23850  filuni  23868  ptcmplem2  24036  itg1climres  25699  mbfi1fseqlem4  25703  dvferm1lem  25969  dvferm2lem  25971  dvferm  25973  dvivthlem1  25993  coeeq2  26225  coe1termlem  26241  isppw  27095  dchrelbasd  27220  lgsne0  27316  wlkvv  29713  eldm3  35989  brfvimex  44470  brovmptimex  44471  clsneibex  44546  neicvgbex  44556  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