Metamath Proof Explorer


Theorem sbbid

Description: Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993) Remove dependency on ax-10 and ax-13 . (Revised by Wolf Lammen, 24-Nov-2022) Revise df-sb . (Revised by Steven Nguyen, 11-Jul-2023)

Ref Expression
Hypotheses sbbid.1 x φ
sbbid.2 φ ψ χ
Assertion sbbid φ y x ψ y x χ

Proof

Step Hyp Ref Expression
1 sbbid.1 x φ
2 sbbid.2 φ ψ χ
3 1 2 alrimi φ x ψ χ
4 spsbbi x ψ χ y x ψ y x χ
5 3 4 syl φ y x ψ y x χ