DEFINITION and3_ind()
TYPE =
       ∀P0:Prop.∀P1:Prop.∀P2:Prop.∀P:Prop.(P0→P1→P2→P)→(and3 P0 P1 P2)→P
BODY =
Show proof