Theorem necon1ai 2982

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

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

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 2956

This theorem is used by:  necon1i  2988  opnz  5442  inisegn0  6098  iotan0  6532  iotan0OLD  6533  tz6.12i  6916  fvfundmfvn0  6930  brfvopabrbr  6995  elfvmptrab1  7027  brovpreldm  8104  brovex  8246  brwitnlem  8522  cantnflem1  9697  carddomi2  10058  rankcf  10869  eliooxr  13542  iccssioo2  13557  elfzoel1  13798  elfzoel2  13799  ismnd  18935  lactghmga  19628  pmtrmvd  19679  mpfrcl  22403  mhpsclcl  22477  fsubbas  24195  filuni  24213  ptcmplem2  24381  itg1climres  26044  mbfi1fseqlem4  26048  dvferm1lem  26313  dvferm2lem  26315  dvferm  26317  dvivthlem1  26337  coeeq2  26570  coe1termlem  26586  isppw  27450  dchrelbasd  27575  lgsne0  27671  wlkvv  30216  eldm3  36622  brfvimex  45135  brovmptimex  45136  clsneibex  45211  neicvgbex  45221  iotan0aiotaex  48271  afvnufveq  48325  gricrcl  49120  grlicrcl  49213  grilcbri2  49217  ovconstbrd  50081  ovconstbrn0d  50082  elovconstbrd  50083  discsubc  50286  oppfrcl  50352  oppfrcl2  50353  oppfrcl3  50354  eloppf  50357  eloppf2  50358  oppcup3  50433  oppc1stflem  50517  catcrcl  50638