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	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
	Assertion	sbimdv	⊢ ( 𝜑 → ( [ 𝑡 / 𝑥 ] 𝜓 → [ 𝑡 / 𝑥 ] 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		sbimdv.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2	1	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ( 𝜓 → 𝜒 ) )
3		spsbim	⊢ ( ∀ 𝑥 ( 𝜓 → 𝜒 ) → ( [ 𝑡 / 𝑥 ] 𝜓 → [ 𝑡 / 𝑥 ] 𝜒 ) )
4	2 3	syl	⊢ ( 𝜑 → ( [ 𝑡 / 𝑥 ] 𝜓 → [ 𝑡 / 𝑥 ] 𝜒 ) )