Metamath Proof Explorer

Axiom ax-4

Description: Axiom of Quantified Implication. Axiom C4 of Monk2 p. 105 and Theorem 19.20 of Margaris p. 90. It is restated as alim for labeling consistency. It should be used only by alim . (Contributed by NM, 21-May-2008) Use alim instead. (New usage is discouraged.)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx ${setvar}{x}$
1 wph ${wff}{\phi }$
2 wps ${wff}{\psi }$
3 1 2 wi ${wff}\left({\phi }\to {\psi }\right)$
4 3 0 wal ${wff}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
5 1 0 wal ${wff}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
6 2 0 wal ${wff}\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }$
7 5 6 wi ${wff}\left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
8 4 7 wi ${wff}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$