Theory Transport_Implies

✐‹creator "Kevin Kappelmann"›
theory Transport_Implies
  imports
    Function_Relators
    Reverse_Implies
begin

lemma Fun_Rel_iff_imp_imp: "((⟷) ⇛ (⟷) ⇛ (⟷)) (⟶) (⟶)"
  by auto

lemma Fun_Rel_imp_imp_imp: "((⟵) ⇛ (⟶) ⇛ (⟶)) (⟶) (⟶)"
  by auto

lemma Fun_Rel_rev_imp_imp_imp: "((⟶) ⇛ (⟵) ⇛ (⟵)) (⟶) (⟶)"
  by auto

lemma Fun_Rel_iff_rev_imp_rev_imp: "((⟷) ⇛ (⟷) ⇛ (⟷)) (⟵) (⟵)"
  by auto

lemma Fun_Rel_imp_rev_imp_rev_imp: "((⟶) ⇛ (⟵) ⇛ (⟶)) (⟵) (⟵)"
  by force

lemma Fun_Rel_rev_imp_rev_imp_rev_imp: "((⟵) ⇛ (⟶) ⇛ (⟵)) (⟵) (⟵)"
  by force

end