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  5433  inisegn0  6069  iotan0  6501  tz6.12i  6886  fvfundmfvn0  6901  brfvopabrbr  6965  elfvmptrab1  6996  brovpreldm  8068  brovex  8201  brwitnlem  8471  cantnflem1  9642  carddomi2  9923  rankcf  10730  eliooxr  13365  iccssioo2  13380  elfzoel1  13618  elfzoel2  13619  ismnd  18664  lactghmga  19335  pmtrmvd  19386  mpfrcl  21992  mhpsclcl  22034  fsubbas  23754  filuni  23772  ptcmplem2  23940  itg1climres  25615  mbfi1fseqlem4  25619  dvferm1lem  25888  dvferm2lem  25890  dvferm  25892  dvivthlem1  25913  coeeq2  26147  coe1termlem  26163  isppw  27024  dchrelbasd  27150  lgsne0  27246  wlkvv  29555  eldm3  35748  brfvimex  44015  brovmptimex  44016  clsneibex  44091  neicvgbex  44101  iotan0aiotaex  47094  afvnufveq  47148  gricrcl  47914  grlicrcl  47999  grilcbri2  48003  fvconstr  48850  fvconstrn0  48851  fvconstr2  48852  discsubc  49053  oppfrcl  49117  oppfrcl2  49118  oppfrcl3  49119  eloppf  49122  eloppf2  49123  oppcup3  49198  oppc1stflem  49276  catcrcl  49384