Metamath Proof Explorer

Theorem mooran1

Description: "At most one" imports disjunction to conjunction. (Contributed by NM, 5-Apr-2004) (Proof shortened by Andrew Salmon, 9-Jul-2011)

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

Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({\phi }\wedge {\psi }\right)\to {\phi }$
2 1 moimi ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$
3 moan ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$
4 2 3 jaoi ${⊢}\left({\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\vee {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$