Theorem sbequiOLD

Obsolete version of sbequ as of 10-Aug-2026, as per [conventions], paragraph "Biconditional". (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 15-Sep-2018.) (Proof shortened by Steven Nguyen, 7-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash x' = y' \rightarrow [ x' / z ] \, \varphi \rightarrow [ y' / z ] \, \varphi \)
Proof
sbequ
biimpd _