Metamath Proof Explorer

Theorem hba1w

Description: Weak version of hba1 . See comments for ax10w . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017) (Proof shortened by Wolf Lammen, 10-Oct-2021)

Ref Expression
Hypothesis hbn1w.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion hba1w ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$

Proof

Step Hyp Ref Expression
1 hbn1w.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
2 1 cbvalvw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$
3 2 notbii ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }↔¬\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }$
4 3 a1i ${⊢}{x}={y}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }↔¬\forall {y}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
5 4 spw ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
6 5 con2i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
7 4 hbn1w ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
8 1 hbn1w ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
9 8 con1i ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
10 9 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$
11 6 7 10 3syl ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }$