sbanvOLD

Description: Obsolete version of sban as of 24-Jul-2023. Substitution distributes over conjunction. Version of sban with a disjoint variable condition, not requiring ax-13 . (Contributed by Wolf Lammen, 18-Jan-2023) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	sbanvOLD	$⊢ [y/ x] (φ \land ψ) \leftrightarrow ([y/ x] φ \land [y/ x] ψ)$

Proof

Step	Hyp	Ref	Expression
1		sbn	$⊢ [y/ x] \neg (φ \to \neg ψ) \leftrightarrow \neg [y/ x] (φ \to \neg ψ)$
2		sbimvOLD	$⊢ [y/ x] (φ \to \neg ψ) \leftrightarrow ([y/ x] φ \to [y/ x] \neg ψ)$
3		sbn	$⊢ [y/ x] \neg ψ \leftrightarrow \neg [y/ x] ψ$
4	3	imbi2i	$⊢ ([y/ x] φ \to [y/ x] \neg ψ) \leftrightarrow ([y/ x] φ \to \neg [y/ x] ψ)$
5	2 4	bitri	$⊢ [y/ x] (φ \to \neg ψ) \leftrightarrow ([y/ x] φ \to \neg [y/ x] ψ)$
6	1 5	xchbinx	$⊢ [y/ x] \neg (φ \to \neg ψ) \leftrightarrow \neg ([y/ x] φ \to \neg [y/ x] ψ)$
7		df-an	$⊢ (φ \land ψ) \leftrightarrow \neg (φ \to \neg ψ)$
8	7	sbbii	$⊢ [y/ x] (φ \land ψ) \leftrightarrow [y/ x] \neg (φ \to \neg ψ)$
9		df-an	$⊢ ([y/ x] φ \land [y/ x] ψ) \leftrightarrow \neg ([y/ x] φ \to \neg [y/ x] ψ)$
10	6 8 9	3bitr4i	$⊢ [y/ x] (φ \land ψ) \leftrightarrow ([y/ x] φ \land [y/ x] ψ)$

Metamath Proof Explorer

Theorem sbanvOLD

Proof