In[]:=
FindEquationalProof[ForAll[x,Implies[Implies[p[x],Implies[q[x],r[x]]],Implies[And[p[x],q[x]],r[x]]]],{}]
Out[]=
ProofObject
In[]:=
FindEquationalProof[identity[x],{ForAll[g,Implies[group[g],And[associative[g],ident[g]]]],ForAll[g,Implies[ident[g],And[identity[g],inverse[g]]]],group[x]}]
Out[]=
ProofObject