# Metamath Proof Explorer

## Theorem sbied

Description: Conversion of implicit substitution to explicit substitution (deduction version of sbie ) Usage of this theorem is discouraged because it depends on ax-13 . See sbiedw , sbiedvw for variants using disjoint variables, but requiring fewer axioms. (Contributed by NM, 30-Jun-1994) (Revised by Mario Carneiro, 4-Oct-2016) (Proof shortened by Wolf Lammen, 24-Jun-2018) (New usage is discouraged.)

Ref Expression
Hypotheses sbied.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
sbied.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
sbied.3 ${⊢}{\phi }\to \left({x}={y}\to \left({\psi }↔{\chi }\right)\right)$
Assertion sbied ${⊢}{\phi }\to \left(\left[{y}/{x}\right]{\psi }↔{\chi }\right)$

### Proof

Step Hyp Ref Expression
1 sbied.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 sbied.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
3 sbied.3 ${⊢}{\phi }\to \left({x}={y}\to \left({\psi }↔{\chi }\right)\right)$
4 1 sbrim ${⊢}\left[{y}/{x}\right]\left({\phi }\to {\psi }\right)↔\left({\phi }\to \left[{y}/{x}\right]{\psi }\right)$
5 1 2 nfim1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\chi }\right)$
6 3 com12 ${⊢}{x}={y}\to \left({\phi }\to \left({\psi }↔{\chi }\right)\right)$
7 6 pm5.74d ${⊢}{x}={y}\to \left(\left({\phi }\to {\psi }\right)↔\left({\phi }\to {\chi }\right)\right)$
8 5 7 sbie ${⊢}\left[{y}/{x}\right]\left({\phi }\to {\psi }\right)↔\left({\phi }\to {\chi }\right)$
9 4 8 bitr3i ${⊢}\left({\phi }\to \left[{y}/{x}\right]{\psi }\right)↔\left({\phi }\to {\chi }\right)$
10 9 pm5.74ri ${⊢}{\phi }\to \left(\left[{y}/{x}\right]{\psi }↔{\chi }\right)$