Theorem necon1ai 2960

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon1i  2966  opnz  5429  inisegn0  6065  iotan0  6490  tz6.12i  6868  fvfundmfvn0  6882  brfvopabrbr  6946  elfvmptrab1  6978  brovpreldm  8041  brovex  8174  brwitnlem  8444  cantnflem1  9610  carddomi2  9894  rankcf  10700  eliooxr  13332  iccssioo2  13347  elfzoel1  13585  elfzoel2  13586  ismnd  18674  lactghmga  19346  pmtrmvd  19397  mpfrcl  22052  mhpsclcl  22102  fsubbas  23823  filuni  23841  ptcmplem2  24009  itg1climres  25683  mbfi1fseqlem4  25687  dvferm1lem  25956  dvferm2lem  25958  dvferm  25960  dvivthlem1  25981  coeeq2  26215  coe1termlem  26231  isppw  27092  dchrelbasd  27218  lgsne0  27314  wlkvv  29712  eldm3  35977  brfvimex  44382  brovmptimex  44383  clsneibex  44458  neicvgbex  44468  iotan0aiotaex  47453  afvnufveq  47507  gricrcl  48274  grlicrcl  48367  grilcbri2  48371  fvconstr  49221  fvconstrn0  49222  fvconstr2  49223  discsubc  49423  oppfrcl  49487  oppfrcl2  49488  oppfrcl3  49489  eloppf  49492  eloppf2  49493  oppcup3  49568  oppc1stflem  49646  catcrcl  49754