Theorem necon1ai 2957

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2930

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 2931

This theorem is referenced by:  necon1i  2963  opnz  5419  inisegn0  6055  iotan0  6480  tz6.12i  6858  fvfundmfvn0  6872  brfvopabrbr  6936  elfvmptrab1  6967  brovpreldm  8029  brovex  8162  brwitnlem  8432  cantnflem1  9596  carddomi2  9880  rankcf  10686  eliooxr  13318  iccssioo2  13333  elfzoel1  13571  elfzoel2  13572  ismnd  18660  lactghmga  19332  pmtrmvd  19383  mpfrcl  22038  mhpsclcl  22088  fsubbas  23809  filuni  23827  ptcmplem2  23995  itg1climres  25669  mbfi1fseqlem4  25673  dvferm1lem  25942  dvferm2lem  25944  dvferm  25946  dvivthlem1  25967  coeeq2  26201  coe1termlem  26217  isppw  27078  dchrelbasd  27204  lgsne0  27300  wlkvv  29649  eldm3  35904  brfvimex  44209  brovmptimex  44210  clsneibex  44285  neicvgbex  44295  iotan0aiotaex  47281  afvnufveq  47335  gricrcl  48102  grlicrcl  48195  grilcbri2  48199  fvconstr  49049  fvconstrn0  49050  fvconstr2  49051  discsubc  49251  oppfrcl  49315  oppfrcl2  49316  oppfrcl3  49317  eloppf  49320  eloppf2  49321  oppcup3  49396  oppc1stflem  49474  catcrcl  49582