Theorem necon1ai 2809

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-ne 2782

This theorem is referenced by:  necon1i  2815  opnz  4868  inisegn0  5416  tz6.12i  6124  elfvdm  6130  fvfundmfvn0  6136  elfvmptrab1  6213  brovpreldm  7141  brovex  7235  brwitnlem  7474  cantnflem1  8469  carddomi2  8679  cdainf  8897  rankcf  9478  1re  9918  eliooxr  12103  iccssioo2  12117  elfzoel1  12337  elfzoel2  12338  ismnd  17120  lactghmga  17647  pmtrmvd  17699  mpfrcl  19339  fsubbas  21481  filuni  21499  ptcmplem2  21667  itg1climres  23287  mbfi1fseqlem4  23291  dvferm1lem  23551  dvferm2lem  23553  dvferm  23555  dvivthlem1  23575  coeeq2  23802  coe1termlem  23818  isppw  24640  dchrelbasd  24764  lgsne0  24860  clwwlknprop  26300  2wlkonot3v  26402  2spthonot3v  26403  eldm3  30905  brfvimex  37344  brovmptimex  37345  clsneibex  37420  neicvgbex  37430  afvnufveq  39876  1wlkvv  40831