Step * 1 1 of Lemma fo-logic-xmiddle


9. Dom@i
10. ((B x) ∨ ((B x)  A))  A@i
⊢ A
BY
FOImpliesElim 10 }

1
9. Dom@i
10. ((B x) ∨ ((B x)  A))  A@i
⊢ (B x) ∨ ((B x)  A)

2
9. Dom@i
10. ((B x) ∨ ((B x)  A))  A@i
11. A@i
⊢ A


Latex:



9.  x  :  Dom@i
10.  ((B  x)  \mvee{}  ((B  x)  {}\mRightarrow{}  A))  {}\mRightarrow{}  A@i
\mvdash{}  A


By

FOImpliesElim  10




Home Index