theorem must_not_eat_meat
theorem must_not_eat_meat
(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))
⋯3 more premises
: A ("we mustn't eat meat" : Prop)