• 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

    • 1

      c
      forall I const

      • 1

        dragon(c)
        ass

        • 1

          green(c)
          ass

          • 1

            d
            forall I const

            • 1

              child(d, c)
              ass

            • 2

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

            • 3

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

            • 4

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

            • 5

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

            • 6

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

            • 7

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

            • 8

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

            • 9

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

            • 10

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

            • 11

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

          • 12

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

        • 13

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

        • 14

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

        • 15

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

      • 16

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

    • 17

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

  • 18

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