Metamath Proof Explorer


Theorem iineq12dv

Description: Equality deduction for indexed intersection. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses iineq12dv.1 φA=B
iineq12dv.2 φxBC=D
Assertion iineq12dv φxAC=xBD

Proof

Step Hyp Ref Expression
1 iineq12dv.1 φA=B
2 iineq12dv.2 φxBC=D
3 1 iineq1d φxAC=xBC
4 2 iineq2dv φxBC=xBD
5 3 4 eqtrd φxAC=xBD