Theorem necon1ai 2952

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon1i  2958  opnz  5416  inisegn0  6049  iotan0  6472  tz6.12i  6848  fvfundmfvn0  6863  brfvopabrbr  6927  elfvmptrab1  6958  brovpreldm  8022  brovex  8155  brwitnlem  8425  cantnflem1  9585  carddomi2  9866  rankcf  10671  eliooxr  13307  iccssioo2  13322  elfzoel1  13560  elfzoel2  13561  ismnd  18611  lactghmga  19284  pmtrmvd  19335  mpfrcl  21990  mhpsclcl  22032  fsubbas  23752  filuni  23770  ptcmplem2  23938  itg1climres  25613  mbfi1fseqlem4  25617  dvferm1lem  25886  dvferm2lem  25888  dvferm  25890  dvivthlem1  25911  coeeq2  26145  coe1termlem  26161  isppw  27022  dchrelbasd  27148  lgsne0  27244  wlkvv  29572  eldm3  35734  brfvimex  43999  brovmptimex  44000  clsneibex  44075  neicvgbex  44085  iotan0aiotaex  47077  afvnufveq  47131  gricrcl  47898  grlicrcl  47991  grilcbri2  47995  fvconstr  48846  fvconstrn0  48847  fvconstr2  48848  discsubc  49049  oppfrcl  49113  oppfrcl2  49114  oppfrcl3  49115  eloppf  49118  eloppf2  49119  oppcup3  49194  oppc1stflem  49272  catcrcl  49380