F:Formula. subformula(F) 
Formula Listp,q:Formula. p
q Formulap,q:Formula. p
q Formulap,q:Formula. p
q Formulax:Formula. 
x Formulax:Var. x Formula
formula)+(formulaformula)+(formulaformula))
is mentioned by
| Thm* F:Formula. subformula(F) Formula List | [subformula_wf] |
| Thm* p,q:Formula. pq Formula | [fimp_wf] |
| Thm* p,q:Formula. pq Formula | [f_or_wf] |
| Thm* p,q:Formula. pq Formula | [fand_wf] |
| Thm* x:Formula. x Formula | [fnot_wf] |
| Thm* x:Var. x Formula | [fvar_wf] |
Try larger context:
ClassicalProps(jlc)