Theorem dfnab2 269

Description: Read from a nilad.

Assertion

Ref	Expression
dfnab2	⊦ ([{x | 𝜑} ≫ y] 𝜓 ⧟ (𝜑 ⊗ [x ≫ a] [a ≫ y] 𝜓))

Distinct variable groups:   𝜑,a   𝜓,a   a,x   a,y

Proof of Theorem dfnab2

Step	Hyp	Ref	Expression

Syntax hints:   ⧟ wlb 55   ⊗ wmc 105  nvar 203  [wre 205  {nnab 266

 WARNING: This theorem has an incomplete proof.

This theorem is referenced by: (None)