Theorem necon2bd 3034

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3018

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 209  df-ne 3019

This theorem is referenced by:  necon4bd  3038  necon4d  3042  minel  4417  disjiun  5055  eceqoveq  8404  en3lp  9079  infpssrlem5  9731  nneo  12069  zeo2  12072  sqrt2irr  15604  bezoutr1  15915  coprm  16057  dfphi2  16113  pltirr  17575  oddvdsnn0  18674  psgnodpmr  20736  supnfcls  22630  flimfnfcls  22638  metds0  23460  metdseq0  23464  metnrmlem1a  23468  sineq0  25111  lgsqr  25929  staddi  30025  stadd3i  30027  eulerpartlems  31620  erdszelem8  32447  finminlem  33668  ordcmp  33797  poimirlem18  34912  poimirlem21  34915  cvrnrefN  36420  trlnidatb  37315