Theorem nfttrcl

Description: Bound variable hypothesis builder for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024)

	Ref	Expression
Hypothesis	nfttrcl.1	$$⊢\underset{\_}{Ⅎ}xR$$
Assertion	nfttrcl	Could not format assertion : No typesetting found for |- F/_ x t++ R with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nfttrcl.1	$$⊢\underset{\_}{Ⅎ}xR$$
2	1	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xR$$
3	2	nfttrcld	Could not format ( T. -> F/_ x t++ R ) : No typesetting found for |- ( T. -> F/_ x t++ R ) with typecode |-
4	3	mptru	Could not format F/_ x t++ R : No typesetting found for |- F/_ x t++ R with typecode |-