Theorem mteqand 3050

Description: A modus tollens deduction for inequality. (Contributed by Steven Nguyen, 1-Jun-2023.)

Hypotheses

Ref	Expression
mteqand.1	⊢ (𝜑 → 𝐶 ≠ 𝐷)
mteqand.2	⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐶 = 𝐷)

Assertion

Ref	Expression
mteqand	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Proof of Theorem mteqand

Step	Hyp	Ref	Expression
1		mteqand.1	. . . 4 ⊢ (𝜑 → 𝐶 ≠ 𝐷)
2	1	neneqd 2964	. . 3 ⊢ (𝜑 → ¬ 𝐶 = 𝐷)
3		mteqand.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐶 = 𝐷)
4	2, 3	mtand 828	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
5	4	neqned 2966	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = 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-an 402  df-ne 2960

This theorem is used by:  isdrngd  21055  imadrhmcl  21087  qsidomlem2  21670  flt0  28002  fltne  28008  tglnpt3  29155  tgaaddcpbl  29385  angmgmaddeu3  29414  prlngmid2  29472  prlngsymquadlem  29474  fracfld  33954  rprmasso  34141  vr1nz  34208  rtelextdg2lem  34441  2sqr3minply  34495  cos9thpiminplylem2  34498  zarcmplem  34596  expeq1d  43585  remul01  43662  remulinvcom  43688  mulgt0b2d  43746  sn-inelr  43755  ricdrng1  43796  prjspersym  43839  prjspreln0  43841  line2x  50081  fucoaltnelem  50709  eufunc  50872