Theorem necon1ai 2972

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2944

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 2945

This theorem is referenced by:  necon1i  2978  opnz  5389  inisegn0  6009  iotan0  6427  tz6.12i  6809  fvfundmfvn0  6821  brfvopabrbr  6881  elfvmptrab1  6911  brovpreldm  7938  brovex  8047  brwitnlem  8346  cantnflem1  9456  carddomi2  9737  rankcf  10542  1re  10984  eliooxr  13146  iccssioo2  13161  elfzoel1  13394  elfzoel2  13395  ismnd  18397  lactghmga  19022  pmtrmvd  19073  mpfrcl  21304  mhpsclcl  21346  fsubbas  23027  filuni  23045  ptcmplem2  23213  itg1climres  24888  mbfi1fseqlem4  24892  dvferm1lem  25157  dvferm2lem  25159  dvferm  25161  dvivthlem1  25181  coeeq2  25412  coe1termlem  25428  isppw  26272  dchrelbasd  26396  lgsne0  26492  wlkvv  28003  eldm3  33737  brfvimex  41643  brovmptimex  41644  clsneibex  41719  neicvgbex  41729  iotan0aiotaex  44596  afvnufveq  44650  fvconstr  46194  fvconstrn0  46195  fvconstr2  46196