theorem c1_by_modus_ponens
theorem c1_by_modus_ponens
(p1 : A ("we have a duty to perfect our moral character" : Prop))
(p2 : A ("when we mistreat animals, we corrupt our moral character" : Prop))
(no_mistreat_bridge : A ("we have a duty to perfect our moral character" : Prop) ∧
        A ("when we mistreat animals, we corrupt our moral character" : Prop) →
          A ("we mustn't mistreat animals" : Prop))
: A ("we mustn't mistreat animals" : Prop)