sbor

Description: Disjunction inside and outside of a substitution are equivalent. (Contributed by NM, 29-Sep-2002)

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

Step	Hyp	Ref	Expression
1		sbim	$⊢ [y/ x] (\neg φ \to ψ) \leftrightarrow ([y/ x] \neg φ \to [y/ x] ψ)$
2		sbn	$⊢ [y/ x] \neg φ \leftrightarrow \neg [y/ x] φ$
3	2	imbi1i	$⊢ ([y/ x] \neg φ \to [y/ x] ψ) \leftrightarrow (\neg [y/ x] φ \to [y/ x] ψ)$
4	1 3	bitri	$⊢ [y/ x] (\neg φ \to ψ) \leftrightarrow (\neg [y/ x] φ \to [y/ x] ψ)$
5		df-or	$⊢ (φ \lor ψ) \leftrightarrow (\neg φ \to ψ)$
6	5	sbbii	$⊢ [y/ x] (φ \lor ψ) \leftrightarrow [y/ x] (\neg φ \to ψ)$
7		df-or	$⊢ ([y/ x] φ \lor [y/ x] ψ) \leftrightarrow (\neg [y/ x] φ \to [y/ x] ψ)$
8	4 6 7	3bitr4i	$⊢ [y/ x] (φ \lor ψ) \leftrightarrow ([y/ x] φ \lor [y/ x] ψ)$

Metamath Proof Explorer