# Metamath Proof Explorer

## Theorem bnj1101

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1101.1 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
bnj1101.2 ${⊢}{\chi }\to {\phi }$
Assertion bnj1101 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\chi }\to {\psi }\right)$

### Proof

Step Hyp Ref Expression
1 bnj1101.1 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
2 bnj1101.2 ${⊢}{\chi }\to {\phi }$
3 pm3.42 ${⊢}\left({\phi }\to {\psi }\right)\to \left(\left({\chi }\wedge {\phi }\right)\to {\psi }\right)$
4 1 3 bnj101 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({\chi }\wedge {\phi }\right)\to {\psi }\right)$
5 2 pm4.71i ${⊢}{\chi }↔\left({\chi }\wedge {\phi }\right)$
6 5 imbi1i ${⊢}\left({\chi }\to {\psi }\right)↔\left(\left({\chi }\wedge {\phi }\right)\to {\psi }\right)$
7 6 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\chi }\to {\psi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left(\left({\chi }\wedge {\phi }\right)\to {\psi }\right)$
8 4 7 mpbir ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\chi }\to {\psi }\right)$