Theorem necon1ai 2955

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  necon1i  2961  opnz  5411  inisegn0  6046  iotan0  6471  tz6.12i  6848  fvfundmfvn0  6862  brfvopabrbr  6926  elfvmptrab1  6957  brovpreldm  8019  brovex  8152  brwitnlem  8422  cantnflem1  9579  carddomi2  9863  rankcf  10668  eliooxr  13304  iccssioo2  13319  elfzoel1  13557  elfzoel2  13558  ismnd  18645  lactghmga  19317  pmtrmvd  19368  mpfrcl  22020  mhpsclcl  22062  fsubbas  23782  filuni  23800  ptcmplem2  23968  itg1climres  25642  mbfi1fseqlem4  25646  dvferm1lem  25915  dvferm2lem  25917  dvferm  25919  dvivthlem1  25940  coeeq2  26174  coe1termlem  26190  isppw  27051  dchrelbasd  27177  lgsne0  27273  wlkvv  29605  eldm3  35805  brfvimex  44067  brovmptimex  44068  clsneibex  44143  neicvgbex  44153  iotan0aiotaex  47132  afvnufveq  47186  gricrcl  47953  grlicrcl  48046  grilcbri2  48050  fvconstr  48901  fvconstrn0  48902  fvconstr2  48903  discsubc  49104  oppfrcl  49168  oppfrcl2  49169  oppfrcl3  49170  eloppf  49173  eloppf2  49174  oppcup3  49249  oppc1stflem  49327  catcrcl  49435