Theorem necon1ai 2974

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  necon1i  2980  opnz  5493  inisegn0  6128  iotan0  6563  tz6.12i  6948  fvfundmfvn0  6963  brfvopabrbr  7026  elfvmptrab1  7057  brovpreldm  8130  brovex  8263  brwitnlem  8563  cantnflem1  9758  carddomi2  10039  rankcf  10846  1re  11290  eliooxr  13465  iccssioo2  13480  elfzoel1  13714  elfzoel2  13715  ismnd  18775  lactghmga  19447  pmtrmvd  19498  mpfrcl  22132  mhpsclcl  22174  fsubbas  23896  filuni  23914  ptcmplem2  24082  itg1climres  25769  mbfi1fseqlem4  25773  dvferm1lem  26042  dvferm2lem  26044  dvferm  26046  dvivthlem1  26067  coeeq2  26301  coe1termlem  26317  isppw  27175  dchrelbasd  27301  lgsne0  27397  wlkvv  29663  eldm3  35723  brfvimex  43988  brovmptimex  43989  clsneibex  44064  neicvgbex  44074  iotan0aiotaex  47008  afvnufveq  47062  gricrcl  47767  grlicrcl  47824  grilcbri2  47828  fvconstr  48569  fvconstrn0  48570  fvconstr2  48571