# Metamath Proof Explorer

## Theorem alrim3con13v

Description: Closed form of alrimi with 2 additional conjuncts having no occurrences of the quantifying variable. This proof is 19.21a3con13vVD automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({\psi }\wedge {\phi }\wedge {\chi }\right)\to {\psi }$
2 1 a1i ${⊢}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\left({\psi }\wedge {\phi }\wedge {\chi }\right)\to {\psi }\right)$
3 ax-5 ${⊢}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }$
4 2 3 syl6 ${⊢}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\left({\psi }\wedge {\phi }\wedge {\chi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
5 simp2 ${⊢}\left({\psi }\wedge {\phi }\wedge {\chi }\right)\to {\phi }$
6 5 imim1i ${⊢}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\left({\psi }\wedge {\phi }\wedge {\chi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
7 simp3 ${⊢}\left({\psi }\wedge {\phi }\wedge {\chi }\right)\to {\chi }$
8 7 a1i ${⊢}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\left({\psi }\wedge {\phi }\wedge {\chi }\right)\to {\chi }\right)$
9 ax-5 ${⊢}{\chi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }$
10 8 9 syl6 ${⊢}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\left({\psi }\wedge {\phi }\wedge {\chi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
11 4 6 10 3jcad ${⊢}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\left({\psi }\wedge {\phi }\wedge {\chi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)\right)$
12 19.26-3an ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\wedge {\chi }\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
13 11 12 syl6ibr ${⊢}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\left({\psi }\wedge {\phi }\wedge {\chi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\psi }\wedge {\phi }\wedge {\chi }\right)\right)$