This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mteqand

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

Ref Expression
Hypotheses mteqand.1 ⊢ φ → C ≠ D
mteqand.2 ⊢ φ ∧ A = B → C = D
Assertion mteqand ⊢ φ → A ≠ B

Proof

Step Hyp Ref Expression
1 mteqand.1 ⊢ φ → C ≠ D
2 mteqand.2 ⊢ φ ∧ A = B → C = D
3 1 neneqd ⊢ φ → ¬ C = D
4 3 2 mtand ⊢ φ → ¬ A = B
5 4 neqned ⊢ φ → A ≠ B