Theorem necon2bd 2976

Description: Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)

Hypothesis

Ref	Expression
necon2bd.1	⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))

Assertion

Ref	Expression
necon2bd	⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))

Proof of Theorem necon2bd

Step	Hyp	Ref	Expression
1		necon2bd.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵))
2		df-ne 2961	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	imbitrdi 254	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
4	3	con2d 135	1 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2960

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2961

This theorem is used by:  necon4bd  2980  necon4d  2984  minel  4426  disjiun  5099  eceqoveq  8822  en3lp  9586  infpssrlem5  10302  nneo  12691  zeo2  12694  sqrt2irr  16322  bezoutr1  16644  coprm  16787  dfphi2  16850  pltirr  18406  oddvdsnn0  19637  psgnodpmr  21769  supnfcls  24206  flimfnfcls  24214  metds0  25037  metdseq0  25041  metnrmlem1a  25045  sineq0  26718  lgsqr  27544  staddi  32627  stadd3i  32629  eulerpartlems  34774  erdszelem8  35703  finminlem  36862  ordcmp  36991  poimirlem18  38322  poimirlem21  38325  cvrnrefN  40089  trlnidatb  40984  flt4lem2  43412