Dérivation Cube (a) de Cube (a) <-> a = a (Fitch)

Question

Je suis en train de prouver quelque chose dans Fitch et je suis coincé sur un pas, j'ai:

1.  Cube(a) <-> a = a

et je veux 2. Cube(a) en tirer.

Je sais qu'il est possible parce que je peux utiliser Ana Con le 2 et la sélection 1. comme prémisse et il dit qu'il est valide.
Est-ce qu'il ya quelqu'un qui peut me dire comment faire cela sans utiliser Ana Con?

Answer 1

(Je n'ai pas une copie de Fitch et n'a jamais utilisé, donc prendre avec une pincée de sel. Mais je suis sûr qu'il a raison.)

D'abord obtenir juste "= a" à l'aide = Intro. (Vous ne avez pas besoin de locaux.) Prenez ensuite que plus votre 1. et appliquer <-> pour obtenir Cube Élim (a)

.