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