Theorem necon1ai 2959

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2932

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 2933

This theorem is referenced by:  necon1i  2965  opnz  5421  inisegn0  6057  iotan0  6482  tz6.12i  6860  fvfundmfvn0  6874  brfvopabrbr  6938  elfvmptrab1  6969  brovpreldm  8031  brovex  8164  brwitnlem  8434  cantnflem1  9598  carddomi2  9882  rankcf  10688  eliooxr  13320  iccssioo2  13335  elfzoel1  13573  elfzoel2  13574  ismnd  18662  lactghmga  19334  pmtrmvd  19385  mpfrcl  22040  mhpsclcl  22090  fsubbas  23811  filuni  23829  ptcmplem2  23997  itg1climres  25671  mbfi1fseqlem4  25675  dvferm1lem  25944  dvferm2lem  25946  dvferm  25948  dvivthlem1  25969  coeeq2  26203  coe1termlem  26219  isppw  27080  dchrelbasd  27206  lgsne0  27302  wlkvv  29700  eldm3  35955  brfvimex  44267  brovmptimex  44268  clsneibex  44343  neicvgbex  44353  iotan0aiotaex  47339  afvnufveq  47393  gricrcl  48160  grlicrcl  48253  grilcbri2  48257  fvconstr  49107  fvconstrn0  49108  fvconstr2  49109  discsubc  49309  oppfrcl  49373  oppfrcl2  49374  oppfrcl3  49375  eloppf  49378  eloppf2  49379  oppcup3  49454  oppc1stflem  49532  catcrcl  49640