# Metamath Proof Explorer

## Theorem 19.30

Description: Theorem 19.30 of Margaris p. 90. (Contributed by NM, 12-Mar-1993) (Proof shortened by Andrew Salmon, 25-May-2011)

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

### Proof

Step Hyp Ref Expression
1 exnal ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 pm2.53 ${⊢}\left({\phi }\vee {\psi }\right)\to \left(¬{\phi }\to {\psi }\right)$
3 2 aleximi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\vee {\psi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}¬{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
4 1 3 syl5bir ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\vee {\psi }\right)\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
5 4 orrd ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\vee {\psi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\vee \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$