$( <MM> <PROOF ASST> THEOREM=
19.21adv
LOC_AFTER=
19.21adv
* Deduction from Theorem 19.21 of [Margaris] p. 90.
h1::19.21adv.1
⊢ (φ → (ψ → χ))
2::ax-17
⊢ (φ → ∀xφ)
3::ax-17
⊢ (ψ → ∀xψ)
qed:2,3,1:19.21ad
⊢ (φ → (ψ → ∀xχ))
$= wph wps wch vx wph vx ax-17 wps vx ax-17 19.21adv.1 19.21ad $.
$d φx
$d ψx
$)