ancoms Show Code edit
# Inference commuting conjunction in antecedent. //Notational convention//:
# We sometimes suffix with "s" the label of an inference that manipulates
# an antecedent, leaving the consequent unchanged. The "s" means that the
# inference eliminates the need for a syllogism ([[syl]]) -type inference
# in a proof.
## Commute Conjunction
thm (ancoms () (ancoms.1 (-> (/\ ph ps) ch)) (-> (/\ ps ph) ch) ps ph ancom ancoms.1 sylbi)
(-> (/\ ps ph) ch)