# Metamath Proof Explorer

## Theorem r19.26

Description: Restricted quantifier version of 19.26 . (Contributed by NM, 28-Jan-1997) (Proof shortened by Andrew Salmon, 30-May-2011)

Ref Expression
Assertion r19.26 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({\phi }\wedge {\psi }\right)\to {\phi }$
2 1 ralimi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
3 simpr ${⊢}\left({\phi }\wedge {\psi }\right)\to {\psi }$
4 3 ralimi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$
5 2 4 jca ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
6 pm3.2 ${⊢}{\phi }\to \left({\psi }\to \left({\phi }\wedge {\psi }\right)\right)$
7 6 ral2imi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)\right)$
8 7 imp ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)$
9 5 8 impbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {\psi }\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$