Metamath Proof Explorer


Theorem cbv2h

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 11-May-1993) (New usage is discouraged.)

Ref Expression
Hypotheses cbv2h.1 φψyψ
cbv2h.2 φχxχ
cbv2h.3 φx=yψχ
Assertion cbv2h xyφxψyχ

Proof

Step Hyp Ref Expression
1 cbv2h.1 φψyψ
2 cbv2h.2 φχxχ
3 cbv2h.3 φx=yψχ
4 biimp ψχψχ
5 3 4 syl6 φx=yψχ
6 1 2 5 cbv1h xyφxψyχ
7 equcomi y=xx=y
8 biimpr ψχχψ
9 7 3 8 syl56 φy=xχψ
10 2 1 9 cbv1h yxφyχxψ
11 10 alcoms xyφyχxψ
12 6 11 impbid xyφxψyχ