Theorem necon1ai 2969

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  necon1i  2975  opnz  5474  inisegn0  6098  iotan0  6534  tz6.12i  6920  fvfundmfvn0  6935  brfvopabrbr  6996  elfvmptrab1  7026  brovpreldm  8075  brovex  8207  brwitnlem  8507  cantnflem1  9684  carddomi2  9965  rankcf  10772  1re  11214  eliooxr  13382  iccssioo2  13397  elfzoel1  13630  elfzoel2  13631  ismnd  18628  lactghmga  19273  pmtrmvd  19324  mpfrcl  21648  mhpsclcl  21690  fsubbas  23371  filuni  23389  ptcmplem2  23557  itg1climres  25232  mbfi1fseqlem4  25236  dvferm1lem  25501  dvferm2lem  25503  dvferm  25505  dvivthlem1  25525  coeeq2  25756  coe1termlem  25772  isppw  26618  dchrelbasd  26742  lgsne0  26838  wlkvv  28884  eldm3  34731  brfvimex  42777  brovmptimex  42778  clsneibex  42853  neicvgbex  42863  iotan0aiotaex  45801  afvnufveq  45855  fvconstr  47522  fvconstrn0  47523  fvconstr2  47524