How do I prove this formal theorem using Ping-Pong $\vdash(( \phi\equiv\psi)\implies\theta[\phi/x])\equiv((\phi\equiv\psi)\implies\theta[\psi/x])$?
I know there is a way using SFL, but, for Ping-Pong, I'm confused. What I tried was doing a Hilbert Style proof (which can be done only for Ping-Pong) and used Axiom 11 (implication/ or intro to implication), but after I got stuck, I tried to convert the disjunction into conjunction. I got from the Ax.11 by using the golden rule (Ax.10) but does not seem to work. Any help be would appreciated.