Theorem necon1ai 2987

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

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

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 2961

This theorem is used by:  necon1i  2993  opnz  5457  inisegn0  6102  iotan0  6530  tz6.12i  6911  fvfundmfvn0  6925  brfvopabrbr  6990  elfvmptrab1  7022  brovpreldm  8090  brovex  8224  brwitnlem  8498  cantnflem1  9665  carddomi2  9972  rankcf  10777  eliooxr  13447  iccssioo2  13462  elfzoel1  13702  elfzoel2  13703  ismnd  18827  lactghmga  19519  pmtrmvd  19570  mpfrcl  22286  mhpsclcl  22360  fsubbas  24075  filuni  24093  ptcmplem2  24261  itg1climres  25924  mbfi1fseqlem4  25928  dvferm1lem  26194  dvferm2lem  26196  dvferm  26198  dvivthlem1  26218  coeeq2  26450  coe1termlem  26466  isppw  27329  dchrelbasd  27454  lgsne0  27550  wlkvv  30034  eldm3  36290  brfvimex  44810  brovmptimex  44811  clsneibex  44886  neicvgbex  44896  iotan0aiotaex  47888  afvnufveq  47942  gricrcl  48737  grlicrcl  48830  grilcbri2  48834  fvconstr  49697  fvconstrn0  49698  fvconstr2  49699  discsubc  49899  oppfrcl  49963  oppfrcl2  49964  oppfrcl3  49965  eloppf  49968  eloppf2  49969  oppcup3  50044  oppc1stflem  50122  catcrcl  50230