Theorem necon1ai 2984

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1560   ≠ wne 2957

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 209  df-ne 2958

This theorem is referenced by:  necon1i  2990  opnz  5441  inisegn0  6087  iotan0  6511  tz6.12i  6893  fvfundmfvn0  6907  brfvopabrbr  6972  elfvmptrab1  7004  brovpreldm  8068  brovex  8202  brwitnlem  8476  cantnflem1  9644  carddomi2  9928  rankcf  10735  eliooxr  13408  iccssioo2  13423  elfzoel1  13662  elfzoel2  13663  ismnd  18771  lactghmga  19445  pmtrmvd  19496  mpfrcl  22135  mhpsclcl  22209  fsubbas  23924  filuni  23942  ptcmplem2  24110  itg1climres  25773  mbfi1fseqlem4  25777  dvferm1lem  26043  dvferm2lem  26045  dvferm  26047  dvivthlem1  26067  coeeq2  26299  coe1termlem  26315  isppw  27175  dchrelbasd  27300  lgsne0  27396  wlkvv  29824  eldm3  36108  brfvimex  44599  brovmptimex  44600  clsneibex  44675  neicvgbex  44685  iotan0aiotaex  47684  afvnufveq  47738  gricrcl  48533  grlicrcl  48626  grilcbri2  48630  fvconstr  49480  fvconstrn0  49481  fvconstr2  49482  discsubc  49682  oppfrcl  49746  oppfrcl2  49747  oppfrcl3  49748  eloppf  49751  eloppf2  49752  oppcup3  49827  oppc1stflem  49905  catcrcl  50013