Theorem sbor

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

	Ref	Expression
Assertion	sbor	|- ( [ y / x ] ( ph \/ ps ) <-> ( [ y / x ] ph \/ [ y / x ] ps ) )

Proof

Step	Hyp	Ref	Expression
1		sbim	|- ( [ y / x ] ( -. ph -> ps ) <-> ( [ y / x ] -. ph -> [ y / x ] ps ) )
2		sbn	|- ( [ y / x ] -. ph <-> -. [ y / x ] ph )
3	2	imbi1i	|- ( ( [ y / x ] -. ph -> [ y / x ] ps ) <-> ( -. [ y / x ] ph -> [ y / x ] ps ) )
4	1 3	bitri	|- ( [ y / x ] ( -. ph -> ps ) <-> ( -. [ y / x ] ph -> [ y / x ] ps ) )
5		df-or	|- ( ( ph \/ ps ) <-> ( -. ph -> ps ) )
6	5	sbbii	|- ( [ y / x ] ( ph \/ ps ) <-> [ y / x ] ( -. ph -> ps ) )
7		df-or	|- ( ( [ y / x ] ph \/ [ y / x ] ps ) <-> ( -. [ y / x ] ph -> [ y / x ] ps ) )
8	4 6 7	3bitr4i	|- ( [ y / x ] ( ph \/ ps ) <-> ( [ y / x ] ph \/ [ y / x ] ps ) )