Theorem necon1ai 2991

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ≠ wne 2964

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 210  df-ne 2965

This theorem is referenced by:  necon1i  2997  opnz  5456  inisegn0  6101  iotan0  6527  tz6.12i  6908  fvfundmfvn0  6922  brfvopabrbr  6987  elfvmptrab1  7019  brovpreldm  8083  brovex  8217  brwitnlem  8491  cantnflem1  9657  carddomi2  9955  rankcf  10761  eliooxr  13430  iccssioo2  13445  elfzoel1  13684  elfzoel2  13685  ismnd  18794  lactghmga  19474  pmtrmvd  19525  mpfrcl  22204  mhpsclcl  22278  fsubbas  23992  filuni  24010  ptcmplem2  24178  itg1climres  25841  mbfi1fseqlem4  25845  dvferm1lem  26111  dvferm2lem  26113  dvferm  26115  dvivthlem1  26135  coeeq2  26367  coe1termlem  26383  isppw  27243  dchrelbasd  27368  lgsne0  27464  wlkvv  29916  eldm3  36151  brfvimex  44643  brovmptimex  44644  clsneibex  44719  neicvgbex  44729  iotan0aiotaex  47718  afvnufveq  47772  gricrcl  48567  grlicrcl  48660  grilcbri2  48664  fvconstr  49524  fvconstrn0  49525  fvconstr2  49526  discsubc  49726  oppfrcl  49790  oppfrcl2  49791  oppfrcl3  49792  eloppf  49795  eloppf2  49796  oppcup3  49871  oppc1stflem  49949  catcrcl  50057