Theorem sbi1
Distribute substitution over implication. (Contributed by NM,
14-May-1993.) Remove dependencies on axioms. (Revised by Steven
Nguyen, 24-Jul-2023.)
Conclusion
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \rightarrow [ y' / x ] \, \varphi \rightarrow [ y' / x ] \, \psi \)
Proof
l0
dfsb
\( \vdash [ y' / x ] \, (\varphi \rightarrow \psi) \leftrightarrow \forall z \, (z = y' \rightarrow \forall x \, (x = z \rightarrow \varphi \rightarrow \psi)) \)
ax-2
al2imi _
imim3i _
l4
al2imi _
\( \vdash \forall z \, (z = y' \rightarrow \forall x \, (x = z \rightarrow \varphi \rightarrow \psi)) \rightarrow \forall z \, (z = y' \rightarrow \forall x \, (x = z \rightarrow \varphi)) \rightarrow \forall z \, (z = y' \rightarrow \forall x \, (x = z \rightarrow \psi)) \)
l5
dfsb
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \forall z \, (z = y' \rightarrow \forall x \, (x = z \rightarrow \varphi)) \)
dfsb
\( \vdash [ y' / x ] \, \psi \leftrightarrow \forall z \, (z = y' \rightarrow \forall x \, (x = z \rightarrow \psi)) \)
3imtr4g l4 l5 _
\( \vdash \forall z \, (z = y' \rightarrow \forall x \, (x = z \rightarrow \varphi \rightarrow \psi)) \rightarrow [ y' / x ] \, \varphi \rightarrow [ y' / x ] \, \psi \)
sylbi l0 _