---

Step * of Lemma face-term-implies_functionality

No Annotations
∀[Gamma:j⊢]. ∀[a,b,c,d:{Gamma ⊢ _:𝔽}].
  (Gamma ⊢ (a ⇐⇒ c) ⇒ Gamma ⊢ (b ⇐⇒ d) ⇒ (Gamma ⊢ (a ⇒ b) ⇐⇒ Gamma ⊢ (c ⇒ d)))
BY
{ (Auto THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[a,b,c,d:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].
    (Gamma  \mvdash{}  (a  \mLeftarrow{}{}\mRightarrow{}  c)  {}\mRightarrow{}  Gamma  \mvdash{}  (b  \mLeftarrow{}{}\mRightarrow{}  d)  {}\mRightarrow{}  (Gamma  \mvdash{}  (a  {}\mRightarrow{}  b)  \mLeftarrow{}{}\mRightarrow{}  Gamma  \mvdash{}  (c  {}\mRightarrow{}  d)))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index