Theorem necon1ai 2959

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

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

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 2933

This theorem is referenced by:  necon1i  2965  opnz  5426  inisegn0  6063  iotan0  6488  tz6.12i  6866  fvfundmfvn0  6880  brfvopabrbr  6944  elfvmptrab1  6976  brovpreldm  8039  brovex  8172  brwitnlem  8442  cantnflem1  9610  carddomi2  9894  rankcf  10700  eliooxr  13357  iccssioo2  13372  elfzoel1  13611  elfzoel2  13612  ismnd  18705  lactghmga  19380  pmtrmvd  19431  mpfrcl  22063  mhpsclcl  22113  fsubbas  23832  filuni  23850  ptcmplem2  24018  itg1climres  25681  mbfi1fseqlem4  25685  dvferm1lem  25951  dvferm2lem  25953  dvferm  25955  dvivthlem1  25975  coeeq2  26207  coe1termlem  26223  isppw  27077  dchrelbasd  27202  lgsne0  27298  wlkvv  29695  eldm3  35943  brfvimex  44453  brovmptimex  44454  clsneibex  44529  neicvgbex  44539  iotan0aiotaex  47541  afvnufveq  47595  gricrcl  48390  grlicrcl  48483  grilcbri2  48487  fvconstr  49337  fvconstrn0  49338  fvconstr2  49339  discsubc  49539  oppfrcl  49603  oppfrcl2  49604  oppfrcl3  49605  eloppf  49608  eloppf2  49609  oppcup3  49684  oppc1stflem  49762  catcrcl  49870