Theorem necon1ai 2959

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1543   ≠ wne 2932

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 210  df-ne 2933

This theorem is referenced by:  necon1i  2965  opnz  5342  inisegn0  5946  iotan0  6348  tz6.12i  6721  fvfundmfvn0  6733  brfvopabrbr  6793  elfvmptrab1  6823  brovpreldm  7835  brovex  7942  brwitnlem  8212  cantnflem1  9282  carddomi2  9551  rankcf  10356  1re  10798  eliooxr  12958  iccssioo2  12973  elfzoel1  13206  elfzoel2  13207  ismnd  18130  lactghmga  18751  pmtrmvd  18802  mpfrcl  20999  mhpsclcl  21041  fsubbas  22718  filuni  22736  ptcmplem2  22904  itg1climres  24566  mbfi1fseqlem4  24570  dvferm1lem  24835  dvferm2lem  24837  dvferm  24839  dvivthlem1  24859  coeeq2  25090  coe1termlem  25106  isppw  25950  dchrelbasd  26074  lgsne0  26170  wlkvv  27668  eldm3  33398  brfvimex  41254  brovmptimex  41255  clsneibex  41330  neicvgbex  41340  iotan0aiotaex  44200  afvnufveq  44254  fvconstr  45799  fvconstrn0  45800  fvconstr2  45801