Theorem necon1ai 2952

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

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

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 207  df-ne 2926

This theorem is referenced by:  necon1i  2958  opnz  5428  inisegn0  6058  iotan0  6489  tz6.12i  6868  fvfundmfvn0  6883  brfvopabrbr  6947  elfvmptrab1  6978  brovpreldm  8045  brovex  8178  brwitnlem  8448  cantnflem1  9618  carddomi2  9899  rankcf  10706  eliooxr  13341  iccssioo2  13356  elfzoel1  13594  elfzoel2  13595  ismnd  18646  lactghmga  19319  pmtrmvd  19370  mpfrcl  22025  mhpsclcl  22067  fsubbas  23787  filuni  23805  ptcmplem2  23973  itg1climres  25648  mbfi1fseqlem4  25652  dvferm1lem  25921  dvferm2lem  25923  dvferm  25925  dvivthlem1  25946  coeeq2  26180  coe1termlem  26196  isppw  27057  dchrelbasd  27183  lgsne0  27279  wlkvv  29607  eldm3  35741  brfvimex  44008  brovmptimex  44009  clsneibex  44084  neicvgbex  44094  iotan0aiotaex  47087  afvnufveq  47141  gricrcl  47907  grlicrcl  47992  grilcbri2  47996  fvconstr  48843  fvconstrn0  48844  fvconstr2  48845  discsubc  49046  oppfrcl  49110  oppfrcl2  49111  oppfrcl3  49112  eloppf  49115  eloppf2  49116  oppcup3  49191  oppc1stflem  49269  catcrcl  49377