Theorem necon1ai 3041

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1531   ≠ wne 3014

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 209  df-ne 3015

This theorem is referenced by:  necon1i  3047  opnz  5356  inisegn0  5954  iotan0  6338  tz6.12i  6689  fvfundmfvn0  6701  brfvopabrbr  6758  elfvmptrab1  6788  brovpreldm  7776  brovex  7880  brwitnlem  8124  cantnflem1  9144  carddomi2  9391  rankcf  10191  1re  10633  eliooxr  12787  iccssioo2  12801  elfzoel1  13028  elfzoel2  13029  ismnd  17906  lactghmga  18525  pmtrmvd  18576  mpfrcl  20290  fsubbas  22467  filuni  22485  ptcmplem2  22653  itg1climres  24307  mbfi1fseqlem4  24311  dvferm1lem  24573  dvferm2lem  24575  dvferm  24577  dvivthlem1  24597  coeeq2  24824  coe1termlem  24840  isppw  25683  dchrelbasd  25807  lgsne0  25903  wlkvv  27400  eldm3  32990  brfvimex  40366  brovmptimex  40367  clsneibex  40442  neicvgbex  40452  iotan0aiotaex  43281  afvnufveq  43336