---

Step * of Lemma decidable__uimplies

∀[P:ℙ]. ∀Q:⋂x:P. ℙ. (Dec(P) ⇒ Dec(Q) supposing P ⇒ Dec(Q supposing P))
BY
{ Auto }

1
.....decidable?..... 
1. [P] : ℙ
2. Q : ⋂x:P. ℙ@i'
3. Dec(P)@i
4. Dec(Q) supposing P@i
⊢ Dec(Q supposing P)

---

Latex:

---

Latex:
\mforall{}[P:\mBbbP{}].  \mforall{}Q:\mcap{}x:P.  \mBbbP{}.  (Dec(P)  {}\mRightarrow{}  Dec(Q)  supposing  P  {}\mRightarrow{}  Dec(Q  supposing  P))


By

---

Latex:
Auto

---

Home Index