• 1

    ∀ x. ((∀ y. (child(y, x) → fly(y))) ∧ dragon(x) → happy(x))
    premise

  • 2

    ∀ x. (green(x) ∧ dragon(x) → fly(x))
    premise

  • 3

    ∀ x. ((∃ y. (parent(y, x) ∧ green(y))) → green(x))
    premise

  • 4

    ∀ z. (∀ x. (child(x, z) ∧ dragon(z) → dragon(x)))
    premise

  • 5

    ∀ x. (∀ y. (child(y, x) → parent(x, y)))
    premise

    • 6

      c
      forall I const

      • 7

        dragon(c)
        ass

        • 8

          green(c)
          ass

          • 9

            d
            forall I const

            • 10

              child(d, c)
              ass

            • 11

              ∀ y. (child(y, c) → parent(c, y))
              ∀E(5)

            • 12

              parent(c, d)
              ∀->E(10, 11)

            • 13

              parent(c, d) ∧ green(c)
              ∧I(12, 8)

            • 14

              ∃ y. (parent(y, d) ∧ green(y))
              ∃I(13)

            • 15

              green(d)
              ∀->E(14, 3)

            • 16

              child(d, c) ∧ dragon(c)
              ∧I(10, 7)

            • 17

              ∀ x. (child(x, c) ∧ dragon(c) → dragon(x))
              ∀E(4)

            • 18

              dragon(d)
              ∀->E(16, 17)

            • 19

              green(d) ∧ dragon(d)
              ∧I(15, 18)

            • 20

              fly(d)
              ∀->E(19, 2)

          • 21

            child(d, c) → fly(d)
            →I(10, 20)

        • 22

          ∀ y. (child(y, c) → fly(y))
          ∀I(9, 21)

        • 23

          (∀ y. (child(y, c) → fly(y))) ∧ dragon(c)
          ∧I(22, 7)

        • 24

          happy(c)
          ∀->E(23, 1)

      • 25

        green(c) → happy(c)
        →I(8, 24)

    • 26

      dragon(c) → (green(c) → happy(c))
      →I(7, 25)

  • 27

    ∀ x. (dragon(x) → (green(x) → happy(x)))
    ∀I(6, 26)