Metamath Proof Explorer


Theorem neeqtrd

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012)

Ref Expression
Hypotheses neeqtrd.1 φ A B
neeqtrd.2 φ B = C
Assertion neeqtrd φ A C

Proof

Step Hyp Ref Expression
1 neeqtrd.1 φ A B
2 neeqtrd.2 φ B = C
3 2 neeq2d φ A B A C
4 1 3 mpbid φ A C