# Metamath Proof Explorer

## Theorem 19.42v

Description: Version of 19.42 with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993)

Ref Expression
Assertion 19.42v ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left({\phi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 19.41v ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge {\phi }\right)$
2 exancom ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\right)$
3 ancom ${⊢}\left({\phi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge {\phi }\right)$
4 1 2 3 3bitr4i ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left({\phi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 5, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}