Theorem necon1ai 2985

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  necon1i  2991  opnz  5455  inisegn0  6100  iotan0  6526  tz6.12i  6907  fvfundmfvn0  6921  brfvopabrbr  6986  elfvmptrab1  7018  brovpreldm  8080  brovex  8214  brwitnlem  8488  cantnflem1  9654  carddomi2  9952  rankcf  10757  eliooxr  13426  iccssioo2  13441  elfzoel1  13681  elfzoel2  13682  ismnd  18790  lactghmga  19470  pmtrmvd  19521  mpfrcl  22236  mhpsclcl  22310  fsubbas  24024  filuni  24042  ptcmplem2  24210  itg1climres  25873  mbfi1fseqlem4  25877  dvferm1lem  26143  dvferm2lem  26145  dvferm  26147  dvivthlem1  26167  coeeq2  26399  coe1termlem  26415  isppw  27278  dchrelbasd  27403  lgsne0  27499  wlkvv  29976  eldm3  36253  brfvimex  44752  brovmptimex  44753  clsneibex  44828  neicvgbex  44838  iotan0aiotaex  47830  afvnufveq  47884  gricrcl  48679  grlicrcl  48772  grilcbri2  48776  fvconstr  49640  fvconstrn0  49641  fvconstr2  49642  discsubc  49842  oppfrcl  49906  oppfrcl2  49907  oppfrcl3  49908  eloppf  49911  eloppf2  49912  oppcup3  49987  oppc1stflem  50065  catcrcl  50173