Description: Obsolete version of mptmpoopabovd as of 13-Dec-2024. (Contributed by Alexander van der Vekens, 8-Nov-2017) (Revised by AV, 15-Jan-2021) (Proof modification is discouraged.) (New usage is discouraged.)