Examples of Proofs with Quantifiers

∀x(Ax ⇒ Bx), ∀x(Bx ⇒ Cx) ⊢ ∀x(Ax ⇒ Cx)
1.) ∀x(Ax ⇒ Bx)                   Hyp
2.) Ax ⇒ Bx                          UI
3.) ∀x(Bx ⇒ Cx)                   Hyp
4.) Bx ⇒ Cx                          UI
5.) Ax ⇒ Cx                          Th5
6.) ∀x(Ax ⇒ Cx)                   UG

∀x(Bx ⇒ Cx), ∃x(Ax ∧ Bx) ⊢ ∃x(Ax ∧ Cx)
1.) ∃x(Ax ∧ Bx)                        Hyp
2.) ∀x(Bx ⇒ Cx)                      Hyp
3.) Ac ∧ Bc                               EI
4.) (Ac ∧ Bc) ⇒ Bc                  Th28
5.) (Ac ∧ Bc) ⇒ Ac                   Th29
6.) Bc                                        mp 3,4
7.) Ac                                        mp 3,5
8.) Bc ⇒ Cc                               UI
9.) Cc                                        mp 6,8
10.) Ac ⇒ [ Cc ⇒ (Ac ∧ Cc)]    Th30
11.) Cc ⇒ (Ac ∧ Cc)                  mp 7,10
12.) (Ac ∧ Cc)                          mp 9,11
13.) ∃x(Ax ∧ Cx)                      EG