Theorem necon2bd 2975

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 2960	. . 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 2959

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 2960

This theorem is used by:  necon4bd  2979  necon4d  2983  minel  4422  disjiun  5096  onelfvnef1  8487  eceqoveq  8881  en3lp  9652  infpssrlem5  10424  nneo  12823  zeo2  12826  sqrt2irr  16461  bezoutr1  16788  coprm  16931  dfphi2  16995  pltirr  18557  oddvdsnn0  19809  psgnodpmr  21951  supnfcls  24394  flimfnfcls  24402  metds0  25225  metdseq0  25229  metnrmlem1a  25233  sineq0  26909  lgsqr  27735  flt4lem2  28034  staddi  32905  stadd3i  32907  eulerpartlems  35103  erdszelem8  36171  finminlem  37321  ordcmp  37450  poimirlem18  38824  poimirlem21  38827  cvrnrefN  40605  trlnidatb  41500