Theorem necon2bd 2972

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 2957	. . 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 2956

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 2957

This theorem is used by:  necon4bd  2976  necon4d  2980  minel  4419  disjiun  5091  onelfvnef1  8442  eceqoveq  8836  en3lp  9608  infpssrlem5  10378  nneo  12776  zeo2  12779  sqrt2irr  16410  bezoutr1  16737  coprm  16880  dfphi2  16944  pltirr  18500  oddvdsnn0  19751  psgnodpmr  21889  supnfcls  24332  flimfnfcls  24340  metds0  25163  metdseq0  25167  metnrmlem1a  25171  sineq0  26845  lgsqr  27671  flt4lem2  27970  staddi  32841  stadd3i  32843  eulerpartlems  34985  erdszelem8  35942  finminlem  37086  ordcmp  37215  poimirlem18  38536  poimirlem21  38539  cvrnrefN  40319  trlnidatb  41214