Metamath Proof Explorer


Theorem rabrabiOLD

Description: Obsolete version of rabrabi as of 12-Oct-2024. (Contributed by AV, 2-Aug-2022) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis rabrabiOLD.1 x=yχφ
Assertion rabrabiOLD xyA|φ|ψ=xA|χψ

Proof

Step Hyp Ref Expression
1 rabrabiOLD.1 x=yχφ
2 1 cbvrabv xA|χ=yA|φ
3 2 rabeqi xxA|χ|ψ=xyA|φ|ψ
4 rabrab xxA|χ|ψ=xA|χψ
5 3 4 eqtr3i xyA|φ|ψ=xA|χψ