$( <MM> <PROOF ASST> THEOREM= 19.21adv  LOC_AFTER= 19.21adv
 
* Deduction from Theorem 19.21 of [Margaris] p. 90.

h1::19.21adv.1      |- (ph -> (ps -> ch))
2::ax-17            |- (ph -> A.xph)
3::ax-17            |- (ps -> A.xps)
qed:2,3,1:19.21ad   |- (ph -> (ps -> A.xch))

$=  wph wps wch vx wph vx ax-17 wps vx ax-17 19.21adv.1 19.21ad $. 
 $d phx
 $d psx
$)