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  5433  inisegn0  6069  iotan0  6501  tz6.12i  6886  fvfundmfvn0  6901  brfvopabrbr  6965  elfvmptrab1  6996  brovpreldm  8068  brovex  8201  brwitnlem  8471  cantnflem1  9642  carddomi2  9923  rankcf  10730  eliooxr  13365  iccssioo2  13380  elfzoel1  13618  elfzoel2  13619  ismnd  18664  lactghmga  19335  pmtrmvd  19386  mpfrcl  21992  mhpsclcl  22034  fsubbas  23754  filuni  23772  ptcmplem2  23940  itg1climres  25615  mbfi1fseqlem4  25619  dvferm1lem  25888  dvferm2lem  25890  dvferm  25892  dvivthlem1  25913  coeeq2  26147  coe1termlem  26163  isppw  27024  dchrelbasd  27150  lgsne0  27246  wlkvv  29555  eldm3  35748  brfvimex  44015  brovmptimex  44016  clsneibex  44091  neicvgbex  44101  iotan0aiotaex  47091  afvnufveq  47145  gricrcl  47911  grlicrcl  47996  grilcbri2  48000  fvconstr  48847  fvconstrn0  48848  fvconstr2  48849  discsubc  49050  oppfrcl  49114  oppfrcl2  49115  oppfrcl3  49116  eloppf  49119  eloppf2  49120  oppcup3  49195  oppc1stflem  49273  catcrcl  49381