Theorem necon1ai 2967

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

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

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 2940

This theorem is referenced by:  necon1i  2973  opnz  5477  inisegn0  6115  iotan0  6550  tz6.12i  6933  fvfundmfvn0  6948  brfvopabrbr  7012  elfvmptrab1  7043  brovpreldm  8115  brovex  8248  brwitnlem  8546  cantnflem1  9730  carddomi2  10011  rankcf  10818  1re  11262  eliooxr  13446  iccssioo2  13461  elfzoel1  13698  elfzoel2  13699  ismnd  18751  lactghmga  19424  pmtrmvd  19475  mpfrcl  22110  mhpsclcl  22152  fsubbas  23876  filuni  23894  ptcmplem2  24062  itg1climres  25750  mbfi1fseqlem4  25754  dvferm1lem  26023  dvferm2lem  26025  dvferm  26027  dvivthlem1  26048  coeeq2  26282  coe1termlem  26298  isppw  27158  dchrelbasd  27284  lgsne0  27380  wlkvv  29646  eldm3  35762  brfvimex  44044  brovmptimex  44045  clsneibex  44120  neicvgbex  44130  iotan0aiotaex  47110  afvnufveq  47164  gricrcl  47888  grlicrcl  47972  grilcbri2  47976  fvconstr  48770  fvconstrn0  48771  fvconstr2  48772