Theorem necon1ai 2968

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2940

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 206  df-ne 2941

This theorem is referenced by:  necon1i  2974  opnz  5412  inisegn0  6030  iotan0  6463  tz6.12i  6847  fvfundmfvn0  6862  brfvopabrbr  6922  elfvmptrab1  6952  brovpreldm  7989  brovex  8100  brwitnlem  8400  cantnflem1  9538  carddomi2  9819  rankcf  10626  1re  11068  eliooxr  13230  iccssioo2  13245  elfzoel1  13478  elfzoel2  13479  ismnd  18477  lactghmga  19101  pmtrmvd  19152  mpfrcl  21393  mhpsclcl  21435  fsubbas  23116  filuni  23134  ptcmplem2  23302  itg1climres  24977  mbfi1fseqlem4  24981  dvferm1lem  25246  dvferm2lem  25248  dvferm  25250  dvivthlem1  25270  coeeq2  25501  coe1termlem  25517  isppw  26361  dchrelbasd  26485  lgsne0  26581  wlkvv  28196  eldm3  33933  brfvimex  41946  brovmptimex  41947  clsneibex  42022  neicvgbex  42032  iotan0aiotaex  44925  afvnufveq  44979  fvconstr  46523  fvconstrn0  46524  fvconstr2  46525