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 1570   ≠ 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  5449  inisegn0  6094  iotan0  6523  tz6.12i  6904  fvfundmfvn0  6918  brfvopabrbr  6983  elfvmptrab1  7015  brovpreldm  8086  brovex  8220  brwitnlem  8494  cantnflem1  9668  carddomi2  9975  rankcf  10786  eliooxr  13457  iccssioo2  13472  elfzoel1  13712  elfzoel2  13713  ismnd  18839  lactghmga  19532  pmtrmvd  19583  mpfrcl  22301  mhpsclcl  22375  fsubbas  24093  filuni  24111  ptcmplem2  24279  itg1climres  25942  mbfi1fseqlem4  25946  dvferm1lem  26211  dvferm2lem  26213  dvferm  26215  dvivthlem1  26235  coeeq2  26468  coe1termlem  26484  isppw  27350  dchrelbasd  27475  lgsne0  27571  wlkvv  30086  eldm3  36340  brfvimex  44866  brovmptimex  44867  clsneibex  44942  neicvgbex  44952  iotan0aiotaex  47981  afvnufveq  48035  gricrcl  48830  grlicrcl  48923  grilcbri2  48927  fvconstr  49790  fvconstrn0  49791  fvconstr2  49792  discsubc  49990  oppfrcl  50054  oppfrcl2  50055  oppfrcl3  50056  eloppf  50059  eloppf2  50060  oppcup3  50135  oppc1stflem  50213  catcrcl  50321