# Metamath Proof Explorer

## Theorem bj-exlimg

Description: The general form of the *exlim* family of theorems: if ph is substituted for ps , then the antecedent expresses a form of nonfreeness of x in ph , so the theorem means that under a nonfreeness condition in a consequent, one can deduce from the universally quantified implication an implication where the antecedent is existentially quantified. Dual of bj-alrimg . (Contributed by BJ, 9-Dec-2023)

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

### Proof

Step Hyp Ref Expression
1 bj-sylget ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\chi }\to {\phi }\right)\to \left(\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to {\psi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\to {\psi }\right)\right)$
2 1 com12 ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to {\psi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\chi }\to {\phi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\chi }\to {\psi }\right)\right)$