**Description:** An equality transitivity deduction. (Contributed by NM, 21-Jun-1993)

Ref | Expression | ||
---|---|---|---|

Hypotheses | eqtrd.1 | $${\u22a2}{\phi}\to {A}={B}$$ | |

eqtrd.2 | $${\u22a2}{\phi}\to {B}={C}$$ | ||

Assertion | eqtrd | $${\u22a2}{\phi}\to {A}={C}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | eqtrd.1 | $${\u22a2}{\phi}\to {A}={B}$$ | |

2 | eqtrd.2 | $${\u22a2}{\phi}\to {B}={C}$$ | |

3 | 2 | eqeq2d | $${\u22a2}{\phi}\to \left({A}={B}\leftrightarrow {A}={C}\right)$$ |

4 | 1 3 | mpbid | $${\u22a2}{\phi}\to {A}={C}$$ |