Description: If a proposition is implied by z e. _V (which is true, see vex ) and two other antecedents, then it is implied by these other antecedents. (Contributed by Peter Mazsa, 16-Oct-2020)