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 128	1 ⊢ (𝐴 ≠ 𝐵 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1632   ≠ 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 197  df-ne 2933

This theorem is referenced by:  necon1i  2965  opnz  5090  inisegn0  5655  tz6.12i  6375  elfvdm  6381  fvfundmfvn0  6387  brfvopabrbr  6441  elfvmptrab1  6467  brovpreldm  7422  brovex  7517  brwitnlem  7756  cantnflem1  8759  carddomi2  8986  cdainf  9206  rankcf  9791  1re  10231  eliooxr  12425  iccssioo2  12439  elfzoel1  12662  elfzoel2  12663  ismnd  17498  lactghmga  18024  pmtrmvd  18076  mpfrcl  19720  fsubbas  21872  filuni  21890  ptcmplem2  22058  itg1climres  23680  mbfi1fseqlem4  23684  dvferm1lem  23946  dvferm2lem  23948  dvferm  23950  dvivthlem1  23970  coeeq2  24197  coe1termlem  24213  isppw  25039  dchrelbasd  25163  lgsne0  25259  wlkvv  26732  eldm3  31958  brfvimex  38826  brovmptimex  38827  clsneibex  38902  neicvgbex  38912  afvnufveq  41733