# Metamath Proof Explorer

## Theorem bj-sblem2

Description: Lemma for substitution. (Contributed by BJ, 23-Jul-2023)

Ref Expression
Assertion bj-sblem2 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left({\chi }\to {\psi }\right)\right)\to \left(\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to {\chi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 19.23v ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\chi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to {\chi }\right)$
2 ax-2 ${⊢}\left({\phi }\to \left({\chi }\to {\psi }\right)\right)\to \left(\left({\phi }\to {\chi }\right)\to \left({\phi }\to {\psi }\right)\right)$
3 2 al2imi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left({\chi }\to {\psi }\right)\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\chi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)$
4 1 3 syl5bir ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left({\chi }\to {\psi }\right)\right)\to \left(\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to {\chi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\right)$