**Description:** Equality deduction for product. (Contributed by Scott Fenton, 4-Dec-2017)

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

Hypothesis | prodeq2sdv.1 | $${\u22a2}{\phi}\to {B}={C}$$ | |

Assertion | prodeq2sdv | $${\u22a2}{\phi}\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}{C}$$ |

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

1 | prodeq2sdv.1 | $${\u22a2}{\phi}\to {B}={C}$$ | |

2 | 1 | adantr | $${\u22a2}\left({\phi}\wedge {k}\in {A}\right)\to {B}={C}$$ |

3 | 2 | prodeq2dv | $${\u22a2}{\phi}\to \prod _{{k}\in {A}}{B}=\prod _{{k}\in {A}}{C}$$ |