In[]:=
FindEquationalProof[ForAll[x,Implies[Implies[p[x],Implies[q[x],r[x]]],Implies[And[p[x],q[x]],r[x]]]],{}]​​
Out[]=
ProofObject
Logic: Predicate/EquationalLogic
Steps: 115
Theorem:
∀
x
((p[x](q[x]r[x]))(p[x]&&q[x]r[x]))

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
Logic: Predicate/EquationalLogic
Steps: 98
Theorem: identity[x]
