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 1541   ≠ 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  5473  inisegn0  6097  iotan0  6533  tz6.12i  6919  fvfundmfvn0  6934  brfvopabrbr  6995  elfvmptrab1  7025  brovpreldm  8077  brovex  8209  brwitnlem  8509  cantnflem1  9686  carddomi2  9967  rankcf  10774  1re  11216  eliooxr  13384  iccssioo2  13399  elfzoel1  13632  elfzoel2  13633  ismnd  18630  lactghmga  19275  pmtrmvd  19326  mpfrcl  21654  mhpsclcl  21696  fsubbas  23378  filuni  23396  ptcmplem2  23564  itg1climres  25239  mbfi1fseqlem4  25243  dvferm1lem  25508  dvferm2lem  25510  dvferm  25512  dvivthlem1  25532  coeeq2  25763  coe1termlem  25779  isppw  26625  dchrelbasd  26749  lgsne0  26845  wlkvv  28922  eldm3  34800  brfvimex  42859  brovmptimex  42860  clsneibex  42935  neicvgbex  42945  iotan0aiotaex  45880  afvnufveq  45934  fvconstr  47600  fvconstrn0  47601  fvconstr2  47602