Theorem necon2bd 3003

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 2988	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	syl6ib 254	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
4	3	con2d 136	1 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 210  df-ne 2988

This theorem is referenced by:  necon4bd  3007  necon4d  3011  minel  4373  disjiun  5017  eceqoveq  8385  en3lp  9061  infpssrlem5  9718  nneo  12054  zeo2  12057  sqrt2irr  15594  bezoutr1  15903  coprm  16045  dfphi2  16101  pltirr  17565  oddvdsnn0  18664  psgnodpmr  20279  supnfcls  22625  flimfnfcls  22633  metds0  23455  metdseq0  23459  metnrmlem1a  23463  sineq0  25116  lgsqr  25935  staddi  30029  stadd3i  30031  eulerpartlems  31728  erdszelem8  32558  finminlem  33779  ordcmp  33908  poimirlem18  35075  poimirlem21  35078  cvrnrefN  36578  trlnidatb  37473