Boolean lattice (BL) theory is arguably the logic of the system of experimental propositions (EPs) of non-quantum physics. Orthomodular lattice (OML) theory is arguably a logic of the system of EPs of quantum physics. There is a fundamental difference between a BL and an OML: the distributive law holds in a BL but not in an OML. Under certain commutative conditions, however, an OML satisfies some restricted variations of the distributive law; among the most well-known of these relationships are the Foulis-Holland Theorems (FHTs) and the Marsden-Herman Theorem (MHT). Several non-, or partially-, automated derivations of the MHT from the FHTs in OML theory can be found in the OML literature. Here I provide what may be the first fully automated derivations of the MHT from the FHTs conjoined with OML, then show that at least two interesting observations can be distilled directly from the listings of those derivations.