Theorem necon2bd 2954

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 2939	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	imbitrdi 251	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝐴 = 𝐵))
4	3	con2d 134	1 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓))

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

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 207  df-ne 2939

This theorem is referenced by:  necon4bd  2958  necon4d  2962  minel  4472  disjiun  5136  eceqoveq  8861  en3lp  9652  infpssrlem5  10345  nneo  12700  zeo2  12703  sqrt2irr  16282  bezoutr1  16603  coprm  16745  dfphi2  16808  pltirr  18393  oddvdsnn0  19577  psgnodpmr  21626  supnfcls  24044  flimfnfcls  24052  metds0  24886  metdseq0  24890  metnrmlem1a  24894  sineq0  26581  lgsqr  27410  staddi  32275  stadd3i  32277  eulerpartlems  34342  erdszelem8  35183  finminlem  36301  ordcmp  36430  poimirlem18  37625  poimirlem21  37628  cvrnrefN  39264  trlnidatb  40160  flt4lem2  42634