Metamath Proof Explorer

Theorem sbimdv

Description: Deduction substituting both sides of an implication, with ph and x disjoint. See also sbimd . (Contributed by Wolf Lammen, 6-May-2023) Revise df-sb . (Revised by Steven Nguyen, 6-Jul-2023)

Ref Expression
Hypothesis sbimdv.1 φ ψ χ
Assertion sbimdv φ t x ψ t x χ


Step Hyp Ref Expression
1 sbimdv.1 φ ψ χ
2 1 alrimiv φ x ψ χ
3 spsbim x ψ χ t x ψ t x χ
4 2 3 syl φ t x ψ t x χ