Theorem necon1ai 2958

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534   ≠ wne 2930

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 206  df-ne 2931

This theorem is referenced by:  necon1i  2964  opnz  5471  inisegn0  6100  iotan0  6536  tz6.12i  6921  fvfundmfvn0  6936  brfvopabrbr  6998  elfvmptrab1  7029  brovpreldm  8095  brovex  8229  brwitnlem  8529  cantnflem1  9725  carddomi2  10006  rankcf  10811  1re  11255  eliooxr  13430  iccssioo2  13445  elfzoel1  13678  elfzoel2  13679  ismnd  18725  lactghmga  19399  pmtrmvd  19450  mpfrcl  22096  mhpsclcl  22137  fsubbas  23859  filuni  23877  ptcmplem2  24045  itg1climres  25732  mbfi1fseqlem4  25736  dvferm1lem  26004  dvferm2lem  26006  dvferm  26008  dvivthlem1  26029  coeeq2  26266  coe1termlem  26282  isppw  27139  dchrelbasd  27265  lgsne0  27361  wlkvv  29561  eldm3  35596  brfvimex  43730  brovmptimex  43731  clsneibex  43806  neicvgbex  43816  iotan0aiotaex  46742  afvnufveq  46796  gricrcl  47498  grlicrcl  47533  grilcbri2  47537  fvconstr  48259  fvconstrn0  48260  fvconstr2  48261