Metamath Proof Explorer

Theorem bj-alanim

Description: Closed form of alanimi . (Contributed by BJ, 6-May-2019)

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

Proof

Step Hyp Ref Expression
1 pm3.3 ${⊢}\left(\left({\phi }\wedge {\psi }\right)\to {\chi }\right)\to \left({\phi }\to \left({\psi }\to {\chi }\right)\right)$
2 1 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {\chi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left({\psi }\to {\chi }\right)\right)$
3 al2im ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left({\psi }\to {\chi }\right)\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)\right)$
4 2 3 syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {\chi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)\right)$
5 4 impd ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {\chi }\right)\to \left(\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}{\chi }\right)$