Metamath Proof Explorer


Theorem 2sbbid

Description: Deduction doubly substituting both sides of a biconditional. (Contributed by AV, 30-Jul-2023)

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

Proof

Step Hyp Ref Expression
1 sbbid.1 xφ
2 sbbid.2 φψχ
3 2sbbid.1 yφ
4 3 2 sbbid φuyψuyχ
5 1 4 sbbid φtxuyψtxuyχ