Theorem abre2 238

Description: Proper substitution into the right side of ≫ (which is free of that variable).

Assertion

Ref	Expression
abre2	⊦ ([x ≫ y] νa𝜑 ⧟ [a ≔ y] [x ≫ y] νa𝜑)

Distinct variable groups:   a,x   a,y

Proof of Theorem abre2

Step	Hyp	Ref	Expression

Syntax hints:   ⧟ wlb 55  nvar 203  [wre 205  νwnu 206  [wsub 207

 WARNING: This theorem has an incomplete proof.

This theorem is referenced by: (None)