This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ φ \to (ψ \to χ)$
	Assertion	sbimdv	$⊢ φ \to ([t/ x] ψ \to [t/ x] χ)$

Proof

Step	Hyp	Ref	Expression
1		sbimdv.1	$⊢ φ \to (ψ \to χ)$
2	1	alrimiv	$⊢ φ \to \forall x (ψ \to χ)$
3		spsbim	$⊢ \forall x (ψ \to χ) \to ([t/ x] ψ \to [t/ x] χ)$
4	2 3	syl	$⊢ φ \to ([t/ x] ψ \to [t/ x] χ)$