# LPL ( language proof and logic) - FITCH - 14.12

what's wrong with the last line in my proof? i can't understand the error on line 21 i wrote the important line of the proof :

18 - `∀z (Cube(z) → (z = c ∨ z = f))`

19 - `∃y (Cube(c) ∧ Cube(y) ∧ c ≠ y)`

20 - `∃y (Cube(c) ∧ Cube(y) ∧ c ≠ y) ∧ ∀z (Cube(z) → (z = c ∨ z = f))`

21 - `∃x ∃y (Cube(x) ∧ Cube(y) ∧ x ≠ y ∧ ∀z (Cube(z) → (z = x ∨ z = y)))`

EDIT

NOW IT WORK BUT I CAN'T USE FO CON. HOW CAN I WROTE THE SAME LINE WITHOUT USE FO CON? • 21 has an existential quant more than 20: this need a new ∃-intro... – Mauro ALLEGRANZA Dec 28 '17 at 8:59
• @MauroALLEGRANZA i tried but it doesn't work. can you tell me what line i have to select? – Taioli Francesco Dec 28 '17 at 9:19
• From 20 to 21 the z=f has been rewritten as z=y. Whu ? – Mauro ALLEGRANZA Dec 28 '17 at 9:26
• @MauroALLEGRANZA it's a mine error because the ∃-quant doesn't take the ∀z part. How can include the ∀z(..) inside the ∃ intro in the line 20? – Taioli Francesco Dec 28 '17 at 9:33
• @MauroALLEGRANZA i edit the question – Taioli Francesco Dec 28 '17 at 12:17