Theorem necon1ai 2970

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 2943

This theorem is referenced by:  necon1i  2976  opnz  5382  inisegn0  5995  iotan0  6408  tz6.12i  6782  fvfundmfvn0  6794  brfvopabrbr  6854  elfvmptrab1  6884  brovpreldm  7900  brovex  8009  brwitnlem  8299  cantnflem1  9377  carddomi2  9659  rankcf  10464  1re  10906  eliooxr  13066  iccssioo2  13081  elfzoel1  13314  elfzoel2  13315  ismnd  18303  lactghmga  18928  pmtrmvd  18979  mpfrcl  21205  mhpsclcl  21247  fsubbas  22926  filuni  22944  ptcmplem2  23112  itg1climres  24784  mbfi1fseqlem4  24788  dvferm1lem  25053  dvferm2lem  25055  dvferm  25057  dvivthlem1  25077  coeeq2  25308  coe1termlem  25324  isppw  26168  dchrelbasd  26292  lgsne0  26388  wlkvv  27896  eldm3  33634  brfvimex  41525  brovmptimex  41526  clsneibex  41601  neicvgbex  41611  iotan0aiotaex  44472  afvnufveq  44526  fvconstr  46071  fvconstrn0  46072  fvconstr2  46073