Theorem necon1ai 2821

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1483   ≠ wne 2794

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 197  df-ne 2795

This theorem is referenced by:  necon1i  2827  opnz  4942  inisegn0  5497  tz6.12i  6214  elfvdm  6220  fvfundmfvn0  6226  brfvopabrbr  6279  elfvmptrab1  6305  brovpreldm  7254  brovex  7348  brwitnlem  7587  cantnflem1  8586  carddomi2  8796  cdainf  9014  rankcf  9599  1re  10039  eliooxr  12232  iccssioo2  12246  elfzoel1  12468  elfzoel2  12469  ismnd  17297  lactghmga  17824  pmtrmvd  17876  mpfrcl  19518  fsubbas  21671  filuni  21689  ptcmplem2  21857  itg1climres  23481  mbfi1fseqlem4  23485  dvferm1lem  23747  dvferm2lem  23749  dvferm  23751  dvivthlem1  23771  coeeq2  23998  coe1termlem  24014  isppw  24840  dchrelbasd  24964  lgsne0  25060  wlkvv  26522  eldm3  31651  brfvimex  38324  brovmptimex  38325  clsneibex  38400  neicvgbex  38410  afvnufveq  41227