sbimdvOLD

Description: Obsolete version of sbimdv as of 6-Jul-2023. Deduction substituting both sides of an implication, with ph and x disjoint. See also sbimd . (Contributed by Wolf Lammen, 6-May-2023) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	sbimdvOLD.2	$⊢ φ \to (ψ \to χ)$
	Assertion	sbimdvOLD	$⊢ φ \to ([y/ x] ψ \to [y/ x] χ)$

Proof

Step	Hyp	Ref	Expression
1		sbimdvOLD.2	$⊢ φ \to (ψ \to χ)$
2	1	imim2d	$⊢ φ \to ((x = y \to ψ) \to (x = y \to χ))$
3	1	anim2d	$⊢ φ \to ((x = y \land ψ) \to (x = y \land χ))$
4	3	eximdv	$⊢ φ \to (\exists x (x = y \land ψ) \to \exists x (x = y \land χ))$
5	2 4	anim12d	$⊢ φ \to (((x = y \to ψ) \land \exists x (x = y \land ψ)) \to ((x = y \to χ) \land \exists x (x = y \land χ)))$
6		dfsb1	$⊢ [y/ x] ψ \leftrightarrow ((x = y \to ψ) \land \exists x (x = y \land ψ))$
7		dfsb1	$⊢ [y/ x] χ \leftrightarrow ((x = y \to χ) \land \exists x (x = y \land χ))$
8	5 6 7	3imtr4g	$⊢ φ \to ([y/ x] ψ \to [y/ x] χ)$

Metamath Proof Explorer

Theorem sbimdvOLD

Proof