Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Lemmas for substitution
Next ⟩
bj-sbf3
Metamath Proof Explorer
Ascii
Structured
Table of Contents - 21.20.4.22. Lemmas for substitution
bj-sbf3
bj-sbf4