---

Step * of Lemma and_preserved_by2

∀[T:Type]. ∀[P,Q:T ⟶ ℙ]. ∀[R:T ⟶ T ⟶ T ⟶ ℙ].
  ((ternary) R preserves P  ⇒ (ternary) R preserves Q  ⇒ (ternary) R preserves P ∧ Q )
BY
{ (((Unfolds ``prop_and preserved_by2`` 0 THEN Reduce 0) THEN Auto) THEN EasyHyp) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P,Q:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    ((ternary)  R  preserves  P    {}\mRightarrow{}  (ternary)  R  preserves  Q    {}\mRightarrow{}  (ternary)  R  preserves  P  \mwedge{}  Q  )


By

---

Latex:
(((Unfolds  ``prop\_and  preserved\_by2``  0  THEN  Reduce  0)  THEN  Auto)  THEN  EasyHyp)

---

Home Index