Theorem necon1ai 3042

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ≠ wne 3015

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 209  df-ne 3016

This theorem is referenced by:  necon1i  3048  opnz  5362  inisegn0  5958  iotan0  6342  tz6.12i  6693  fvfundmfvn0  6705  brfvopabrbr  6762  elfvmptrab1  6792  brovpreldm  7781  brovex  7885  brwitnlem  8129  cantnflem1  9149  carddomi2  9396  rankcf  10196  1re  10638  eliooxr  12793  iccssioo2  12807  elfzoel1  13034  elfzoel2  13035  ismnd  17910  lactghmga  18529  pmtrmvd  18580  mpfrcl  20294  fsubbas  22471  filuni  22489  ptcmplem2  22657  itg1climres  24311  mbfi1fseqlem4  24315  dvferm1lem  24579  dvferm2lem  24581  dvferm  24583  dvivthlem1  24603  coeeq2  24830  coe1termlem  24846  isppw  25689  dchrelbasd  25813  lgsne0  25909  wlkvv  27406  eldm3  33021  brfvimex  40450  brovmptimex  40451  clsneibex  40526  neicvgbex  40536  iotan0aiotaex  43365  afvnufveq  43420