Theorem necon1ai 2986

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

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

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 2960

This theorem is used by:  necon1i  2992  opnz  5449  inisegn0  6114  iotan0  6555  iotan0OLD  6556  tz6.12i  6942  fvfundmfvn0  6956  brfvopabrbr  7021  elfvmptrab1  7053  brovpreldm  8135  brovex  8277  brwitnlem  8553  cantnflem1  9727  carddomi2  10088  rankcf  10901  eliooxr  13575  iccssioo2  13590  elfzoel1  13831  elfzoel2  13832  ismnd  18976  lactghmga  19670  pmtrmvd  19721  mpfrcl  22449  mhpsclcl  22523  fsubbas  24241  filuni  24259  ptcmplem2  24427  itg1climres  26090  mbfi1fseqlem4  26094  dvferm1lem  26359  dvferm2lem  26361  dvferm  26363  dvivthlem1  26383  coeeq2  26616  coe1termlem  26632  isppw  27498  dchrelbasd  27623  lgsne0  27719  wlkvv  30264  eldm3  36741  brfvimex  45287  brovmptimex  45288  clsneibex  45363  neicvgbex  45373  iotan0aiotaex  48436  afvnufveq  48490  gricrcl  49285  grlicrcl  49378  grilcbri2  49382  ovconstbrd  50304  ovconstbrn0d  50305  elovconstbrd  50306  discsubc  50509  oppfrcl  50575  oppfrcl2  50576  oppfrcl3  50577  eloppf  50580  eloppf2  50581  oppcup3  50656  oppc1stflem  50740  catcrcl  50861