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 131	1 ⊢ (𝐴 ≠ 𝐵 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1507   ≠ 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 199  df-ne 2965

This theorem is referenced by:  necon1i  2997  opnz  5219  inisegn0  5799  tz6.12i  6523  elfvdmOLD  6530  fvfundmfvn0  6536  brfvopabrbr  6590  elfvmptrab1  6618  brovpreldm  7589  brovex  7688  brwitnlem  7930  cantnflem1  8942  carddomi2  9189  rankcf  9993  1re  10435  eliooxr  12608  iccssioo2  12622  elfzoel1  12849  elfzoel2  12850  ismnd  17759  lactghmga  18287  pmtrmvd  18339  mpfrcl  20005  fsubbas  22173  filuni  22191  ptcmplem2  22359  itg1climres  24012  mbfi1fseqlem4  24016  dvferm1lem  24278  dvferm2lem  24280  dvferm  24282  dvivthlem1  24302  coeeq2  24529  coe1termlem  24545  isppw  25387  dchrelbasd  25511  lgsne0  25607  wlkvv  27105  eldm3  32487  brfvimex  39717  brovmptimex  39718  clsneibex  39793  neicvgbex  39803  iotan0aiotaex  42676  afvnufveq  42731