Theorem necon1ai 2983

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  necon1i  2989  opnz  5442  inisegn0  6096  iotan0  6527  tz6.12i  6909  fvfundmfvn0  6923  brfvopabrbr  6988  elfvmptrab1  7020  brovpreldm  8098  brovex  8232  brwitnlem  8508  cantnflem1  9683  carddomi2  10044  rankcf  10855  eliooxr  13528  iccssioo2  13543  elfzoel1  13784  elfzoel2  13785  ismnd  18919  lactghmga  19612  pmtrmvd  19663  mpfrcl  22387  mhpsclcl  22461  fsubbas  24179  filuni  24197  ptcmplem2  24365  itg1climres  26028  mbfi1fseqlem4  26032  dvferm1lem  26297  dvferm2lem  26299  dvferm  26301  dvivthlem1  26321  coeeq2  26554  coe1termlem  26570  isppw  27434  dchrelbasd  27559  lgsne0  27655  wlkvv  30200  eldm3  36505  brfvimex  45011  brovmptimex  45012  clsneibex  45087  neicvgbex  45097  iotan0aiotaex  48132  afvnufveq  48186  gricrcl  48981  grlicrcl  49074  grilcbri2  49078  ovconstbrd  49941  ovconstbrn0d  49942  elovconstbrd  49943  discsubc  50141  oppfrcl  50205  oppfrcl2  50206  oppfrcl3  50207  eloppf  50210  eloppf2  50211  oppcup3  50286  oppc1stflem  50364  catcrcl  50472