Description: A Virtual deduction elimination rule. syl is el1 without virtual deductions. (Contributed by Alan Sare, 23-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).
|- ( ps -> ch )
|- (. ph ->. ch ).
|- ( ph -> ps )
|- ( ph -> ch )