$( <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
$)