Theorem sbor
Disjunction inside and outside of a substitution are equivalent.
(Contributed by NM, 29-Sep-2002.)
Conclusion
\( \vdash [ y' / x ] \, (\varphi \vee \psi) \leftrightarrow [ y' / x ] \, \varphi \vee [ y' / x ] \, \psi \)
Proof
l0
sbim
\( \vdash [ y' / x ] \, (\neg \varphi \rightarrow \psi) \leftrightarrow [ y' / x ] \, (\neg \varphi) \rightarrow [ y' / x ] \, \psi \)
sbn
imbi1i _
\( \vdash [ y' / x ] \, (\neg \varphi) \rightarrow [ y' / x ] \, \psi \leftrightarrow \neg [ y' / x ] \, \varphi \rightarrow [ y' / x ] \, \psi \)
l3
bitri l0 _
\( \vdash [ y' / x ] \, (\neg \varphi \rightarrow \psi) \leftrightarrow \neg [ y' / x ] \, \varphi \rightarrow [ y' / x ] \, \psi \)
df-or
l5
sbbii _
\( \vdash [ y' / x ] \, (\varphi \vee \psi) \leftrightarrow [ y' / x ] \, (\neg \varphi \rightarrow \psi) \)
df-or
\( \vdash [ y' / x ] \, \varphi \vee [ y' / x ] \, \psi \leftrightarrow \neg [ y' / x ] \, \varphi \rightarrow [ y' / x ] \, \psi \)
3bitr4i l3 l5 _