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 1540   ≠ 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  5453  inisegn0  6090  iotan0  6526  tz6.12i  6909  fvfundmfvn0  6924  brfvopabrbr  6988  elfvmptrab1  7019  brovpreldm  8093  brovex  8226  brwitnlem  8524  cantnflem1  9708  carddomi2  9989  rankcf  10796  1re  11240  eliooxr  13426  iccssioo2  13441  elfzoel1  13679  elfzoel2  13680  ismnd  18720  lactghmga  19391  pmtrmvd  19442  mpfrcl  22048  mhpsclcl  22090  fsubbas  23810  filuni  23828  ptcmplem2  23996  itg1climres  25672  mbfi1fseqlem4  25676  dvferm1lem  25945  dvferm2lem  25947  dvferm  25949  dvivthlem1  25970  coeeq2  26204  coe1termlem  26220  isppw  27081  dchrelbasd  27207  lgsne0  27303  wlkvv  29612  eldm3  35783  brfvimex  44017  brovmptimex  44018  clsneibex  44093  neicvgbex  44103  iotan0aiotaex  47089  afvnufveq  47143  gricrcl  47894  grlicrcl  47979  grilcbri2  47983  fvconstr  48805  fvconstrn0  48806  fvconstr2  48807  discsubc  48998  oppfrcl  49043  oppfrcl2  49044  oppfrcl3  49045  oppcup3  49109