animal(sparrow) has_feathers(sparrow) ∀ X. ( animal(X) ∧ has_feathers(X) → bird(X) ) -------------------------------------------------------- (∧-I) ---------------------------------------------------------- (∀-E) animal(sparrow) ∧ has_feather(sparrow) animal(sparrow) ∧ has_feathers(sparrow) → bird(sparrow) ------------------------------------------------------------------------------------------------------------------------ (MP) bird(sparrow) ---------------------- (∃-I) ∃X. bird(X)