# Metamath Proof Explorer

## Theorem moantr

Description: Sufficient condition for transitivity of conjunctions inside existential quantifiers. (Contributed by Peter Mazsa, 2-Oct-2018)

Ref Expression
Assertion moantr ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\to \left(\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\chi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 exancom ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\right)$
2 1 anbi1i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)$
3 2 anbi2i ${⊢}\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)\right)↔\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)\right)$
4 3anass ${⊢}\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)↔\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)\right)$
5 3 4 bitr4i ${⊢}\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)\right)↔\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)$
6 mopick2 ${⊢}\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\wedge {\chi }\right)$
7 5 6 sylbi ${⊢}\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\wedge {\chi }\right)$
8 3anass ${⊢}\left({\psi }\wedge {\phi }\wedge {\chi }\right)↔\left({\psi }\wedge \left({\phi }\wedge {\chi }\right)\right)$
9 8 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\wedge {\chi }\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge \left({\phi }\wedge {\chi }\right)\right)$
10 exsimpr ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge \left({\phi }\wedge {\chi }\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\chi }\right)$
11 9 10 sylbi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\wedge {\chi }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\chi }\right)$
12 7 11 syl ${⊢}\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\chi }\right)$
13 impexp ${⊢}\left(\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\chi }\right)\right)↔\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\to \left(\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\chi }\right)\right)\right)$
14 12 13 mpbi ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\to \left(\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\chi }\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\chi }\right)\right)$