Theory MMI_logic_and_sets

(* 
    This file is a part of MMIsar - a translation of Metamath's set.mm to Isabelle 2005 (ZF logic).

    Copyright (C) 2006  Slawomir Kolodynski

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,
INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,
INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

section ‹Logic and sets in Metamatah›

theory MMI_logic_and_sets imports MMI_prelude

begin

subsection‹Basic Metamath theorems›

text‹This section contains Metamath theorems that the more advanced 
  theorems from ‹MMIsar.thy› depend on. Most of these theorems 
  are proven automatically by Isabelle, some have to be proven by hand 
  and some have to be modified to convert from Tarski-Megill 
  metalogic used by Metamath to one based on explicit notion of 
  free and bound variables.›   

(*text{*The next definition is what Metamath $X\in V$ is
  translated to. I am not sure why it works, probably because
  Isabelle does a type inference and the "=" sign
  indicates that both sides are sets.*}

consts
   IsASet :: "i⇒o" ("_ isASet" [90] 90)

defs
  set_def [simp]: "X isASet ≡  X = X"*)

lemma MMI_ax_mp: assumes "φ" and "φ ⟶ ψ" shows "ψ"
  using assms by auto

lemma MMI_sseli: assumes A1: "A ⊆ B"   
   shows "C ∈ A ⟶ C ∈ B"
   using assms by auto

lemma MMI_sselii: assumes A1: "A ⊆ B" and
    A2: "C ∈ A"   
   shows "C ∈ B"
   using assms by auto

lemma MMI_syl: assumes A1: "φ ⟶ ps" and
    A2: "ps ⟶ ch"   
   shows "φ ⟶ ch"
   using assms by auto

lemma MMI_elimhyp: assumes A1: "A = if ( φ , A , B ) ⟶ ( φ ⟷ ψ )" and
    A2: "B = if ( φ , A , B ) ⟶ ( ch ⟷ ψ )" and
    A3: "ch"   
   shows "ψ"
proof -
  { assume "φ"
    with A1 have "ψ" by simp }
  moreover
  { assume "¬φ"
    with A2 A3 have "ψ" by simp }
  ultimately show "ψ" by auto
qed

lemma MMI_neeq1: 
   shows "A = B ⟶ ( A ≠ C ⟷ B ≠ C )"
  by auto

lemma MMI_mp2: assumes A1: "φ" and
    A2: "ψ" and
    A3: "φ ⟶ ( ψ ⟶ chi )"   
   shows "chi"
   using assms by auto

lemma MMI_xpex: assumes A1: "A isASet" and
    A2: "B isASet"   
   shows "( A × B ) isASet"
   using assms by auto

lemma MMI_fex: 
   shows 
  "A ∈ C ⟶ ( F : A → B ⟶ F isASet )"
  "A isASet ⟶ ( F : A → B ⟶ F isASet )"
  by auto

lemma MMI_3eqtr4d: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ C = A" and
    A3: "φ ⟶ D = B"   
   shows "φ ⟶ C = D"
   using assms by auto

lemma MMI_3coml: assumes A1: "( φ ∧ ψ ∧ chi ) ⟶ th"   
   shows "( ψ ∧ chi ∧ φ ) ⟶ th"
   using assms by auto

lemma MMI_sylan: assumes A1: "( φ ∧ ψ ) ⟶ chi" and
    A2: "th ⟶ φ"   
   shows "( th ∧ ψ ) ⟶ chi"
   using assms by auto

lemma MMI_3impa: assumes A1: "( ( φ ∧ ψ ) ∧ chi ) ⟶ th"   
   shows "( φ ∧ ψ ∧ chi ) ⟶ th"
   using assms by auto

lemma MMI_3adant2: assumes A1: "( φ ∧ ψ ) ⟶ chi"   
   shows "( φ ∧ th ∧ ψ ) ⟶ chi"
   using assms by auto

lemma MMI_3adant1: assumes A1: "( φ ∧ ψ ) ⟶ chi"   
   shows "( th ∧ φ ∧ ψ ) ⟶ chi"
   using assms by auto

lemma (in MMIsar0) MMI_opreq12d: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ C = D"   
   shows 
  "φ ⟶ ( A \<ca> C ) = ( B \<ca> D )"
  "φ ⟶ ( A ⋅ C ) = ( B ⋅ D )"
  "φ ⟶ ( A \<cs> C ) = ( B \<cs> D )"
  "φ ⟶ ( A \<cdiv> C ) = ( B \<cdiv> D )"
   using assms by auto

lemma MMI_mp2an: assumes A1: "φ" and
    A2: "ψ" and
    A3: "( φ ∧ ψ ) ⟶ chi"   
   shows "chi"
   using assms by auto

lemma MMI_mp3an: assumes A1: "φ" and
    A2: "ψ" and
    A3: "ch" and
    A4: "( φ ∧ ψ ∧ ch ) ⟶ θ"   
   shows "θ"
   using assms by auto

lemma MMI_eqeltrr: assumes A1: "A = B" and
    A2: "A ∈ C"   
   shows "B ∈ C"
   using assms by auto

lemma MMI_eqtr: assumes A1: "A = B" and
    A2: "B = C"   
   shows "A = C"
   using assms by auto

(*********************10-20 ******************************************)

lemma MMI_impbi: assumes A1: "φ ⟶ ψ" and
    A2: "ψ ⟶ φ"   
   shows "φ ⟷ ψ"
proof
  assume "φ" with A1 show "ψ" by simp
next
  assume "ψ" with A2 show "φ" by simp
qed

lemma MMI_mp3an3: assumes A1: "ch" and
    A2: "( φ ∧ ψ ∧ ch ) ⟶ θ"   
   shows "( φ ∧ ψ ) ⟶ θ"
   using assms by auto

lemma MMI_eqeq12d: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ C = D"   
   shows "φ ⟶ ( A = C ⟷ B = D )"
   using assms by auto

lemma MMI_mpan2: assumes A1: "ψ" and
    A2: "( φ ∧ ψ ) ⟶ ch"   
   shows "φ ⟶ ch"
   using assms by auto

lemma (in MMIsar0) MMI_opreq2: 
   shows 
  "A = B ⟶ ( C \<ca> A ) = ( C \<ca> B )"
  "A = B ⟶ ( C ⋅ A ) = ( C ⋅ B )"
  "A = B ⟶ ( C \<cs> A ) = ( C \<cs> B )"
  "A = B ⟶ ( C \<cdiv> A ) = ( C \<cdiv> B )"
  by auto

lemma MMI_syl5bir: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "θ ⟶ ch"   
   shows "φ ⟶ ( θ ⟶ ψ )"
   using assms by auto

lemma MMI_adantr: assumes A1: "φ ⟶ ψ"   
   shows "( φ ∧ ch ) ⟶ ψ"
   using assms by auto

lemma MMI_mpan: assumes A1: "φ" and
    A2: "( φ ∧ ψ ) ⟶ ch"   
   shows "ψ ⟶ ch"
   using assms by auto

lemma MMI_eqeq1d: assumes A1: "φ ⟶ A = B"   
   shows "φ ⟶ ( A = C ⟷ B = C )"
   using assms by auto

lemma (in MMIsar0) MMI_opreq1: 
   shows 
  "A = B ⟶ ( A ⋅ C ) = ( B ⋅ C )"
  "A = B ⟶ ( A \<ca> C ) = ( B \<ca> C )"
  "A = B ⟶ ( A \<cs> C ) = ( B \<cs> C )"
  "A = B ⟶ ( A \<cdiv> C ) = ( B \<cdiv> C )"
  by auto

lemma MMI_syl6eq: assumes A1: "φ ⟶ A = B" and
    A2: "B = C"   
   shows "φ ⟶ A = C"
   using assms by auto

lemma MMI_syl6bi: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "ch ⟶ θ"   
   shows "φ ⟶ ( ψ ⟶ θ )"
   using assms by auto

lemma MMI_imp: assumes A1: "φ ⟶ ( ψ ⟶ ch )"   
   shows "( φ ∧ ψ ) ⟶ ch"
   using assms by auto

lemma MMI_sylibd: assumes A1: "φ ⟶ ( ψ ⟶ ch )" and
    A2: "φ ⟶ ( ch ⟷ θ )"   
   shows "φ ⟶ ( ψ ⟶ θ )"
   using assms by auto

lemma MMI_ex: assumes A1: "( φ ∧ ψ ) ⟶ ch"   
   shows "φ ⟶ ( ψ ⟶ ch )"
   using assms by auto

lemma MMI_r19_23aiv: assumes A1: "∀x.  (x ∈ A  ⟶ (φ(x) ⟶ ψ ))"   
   shows "( ∃ x ∈ A . φ(x) ) ⟶ ψ"
  using assms by auto

lemma MMI_bitr: assumes A1: "φ ⟷ ψ" and
    A2: "ψ ⟷ ch"   
   shows "φ ⟷ ch"
   using assms by auto

lemma MMI_eqeq12i: assumes A1: "A = B" and
    A2: "C = D"   
   shows "A = C ⟷ B = D"
   using assms by auto

lemma MMI_dedth3h: 
  assumes A1: "A = if ( φ , A , D ) ⟶ ( θ ⟷ ta )" and
    A2: "B = if ( ψ , B , R ) ⟶ ( ta ⟷ et )" and
    A3: "C = if ( ch , C , S ) ⟶ ( et ⟷ ze )" and
    A4: "ze"   
   shows "( φ ∧ ψ ∧ ch ) ⟶ θ"
   using assms by auto

lemma MMI_bibi1d: assumes A1: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ( ( ψ ⟷ θ ) ⟷ ( ch ⟷ θ ) )"
   using assms by auto

lemma MMI_eqeq1: 
   shows "A = B ⟶ ( A = C ⟷ B = C )"
  by auto

lemma MMI_bibi12d: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "φ ⟶ ( θ ⟷ ta )"   
   shows "φ ⟶ ( ( ψ ⟷ θ ) ⟷ ( ch ⟷ ta ) )"
   using assms by auto

lemma MMI_eqeq2d: assumes A1: "φ ⟶ A = B"   
   shows "φ ⟶ ( C = A ⟷ C = B )"
   using assms by auto

lemma MMI_eqeq2: 
   shows "A = B ⟶ ( C = A ⟷ C = B )"
  by auto

lemma MMI_elimel: assumes A1: "B ∈ C"   
   shows "if ( A ∈ C , A , B ) ∈ C"
   using assms by auto

lemma MMI_3adant3: assumes A1: "( φ ∧ ψ ) ⟶ ch"   
   shows "( φ ∧ ψ ∧ θ ) ⟶ ch"
   using assms by auto

lemma MMI_bitr3d: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "φ ⟶ ( ψ ⟷ θ )"   
   shows "φ ⟶ ( ch ⟷ θ )"
   using assms by auto

(****************** 20-30 add12t - peano2cn *************)

lemma MMI_3eqtr3d: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ A = C" and
    A3: "φ ⟶ B = D"   
   shows "φ ⟶ C = D"
   using assms by auto

lemma (in MMIsar0) MMI_opreq1d: assumes A1: "φ ⟶ A = B"   
   shows 
  "φ ⟶ ( A \<ca> C ) = ( B \<ca> C )"
  "φ ⟶ ( A \<cs> C ) = ( B \<cs> C )"
  "φ ⟶ ( A ⋅ C ) = ( B ⋅ C )"
  "φ ⟶ ( A \<cdiv> C ) = ( B \<cdiv> C )"
   using assms by auto

lemma MMI_3com12: assumes A1: "( φ ∧ ψ ∧ ch ) ⟶ θ"   
   shows "( ψ ∧ φ ∧ ch ) ⟶ θ"
   using assms by auto

lemma (in MMIsar0) MMI_opreq2d: assumes A1: "φ ⟶ A = B"   
   shows 
  "φ ⟶ ( C \<ca> A ) = ( C \<ca> B )"
  "φ ⟶ ( C \<cs> A ) = ( C \<cs> B )"
  "φ ⟶ ( C ⋅ A ) = ( C ⋅ B )"
  "φ ⟶ ( C \<cdiv> A ) = ( C \<cdiv> B )"
   using assms by auto

lemma MMI_3com23: assumes A1: "( φ ∧ ψ ∧ ch ) ⟶ θ"   
   shows "( φ ∧ ch ∧ ψ ) ⟶ θ"
   using assms by auto

lemma MMI_3expa: assumes A1: "( φ ∧ ψ ∧ ch ) ⟶ θ"   
   shows "( ( φ ∧ ψ ) ∧ ch ) ⟶ θ"
   using assms by auto

lemma MMI_adantrr: assumes A1: "( φ ∧ ψ ) ⟶ ch"   
   shows "( φ ∧ ( ψ ∧ θ ) ) ⟶ ch"
   using assms by auto

lemma MMI_3expb: assumes A1: "( φ ∧ ψ ∧ ch ) ⟶ θ"   
   shows "( φ ∧ ( ψ ∧ ch ) ) ⟶ θ"
   using assms by auto

lemma MMI_an4s: assumes A1: "( ( φ ∧ ψ ) ∧ ( ch ∧ θ ) ) ⟶ τ"   
   shows "( ( φ ∧ ch ) ∧ ( ψ ∧ θ ) ) ⟶ τ"
   using assms by auto

lemma MMI_eqtrd: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ B = C"   
   shows "φ ⟶ A = C"
   using assms by auto

lemma MMI_ad2ant2l: assumes A1: "( φ ∧ ψ ) ⟶ ch"   
   shows "( ( θ ∧ φ ) ∧ ( τ ∧ ψ ) ) ⟶ ch"
   using assms by auto

lemma MMI_pm3_2i: assumes A1: "φ" and
    A2: "ψ"   
   shows "φ ∧ ψ"
   using assms by auto

lemma (in MMIsar0) MMI_opreq2i: assumes A1: "A = B"   
   shows 
  "( C \<ca> A ) = ( C \<ca> B )"
  "( C \<cs> A ) = ( C \<cs> B )"
  "( C ⋅ A ) = ( C ⋅ B )"
   using assms by auto

(************31,33 peano2re, negeu, subval ******************************)

lemma MMI_mpbir2an: assumes A1: "φ ⟷ ( ψ ∧ ch )" and
    A2: "ψ" and
    A3: "ch"   
   shows "φ"
   using assms by auto

lemma MMI_reu4: assumes A1: "∀x y. x = y ⟶ ( φ(x) ⟷ ψ(y) )"   
   shows "( ∃! x . x ∈ A ∧ φ(x) ) ⟷ 
  ( ( ∃ x ∈ A . φ(x) ) ∧ ( ∀ x ∈ A . ∀ y ∈ A . 
  ( ( φ(x) ∧ ψ(y) ) ⟶ x = y ) ) )"
   using assms by auto

lemma MMI_risset: 
   shows "A ∈ B ⟷ ( ∃ x ∈ B . x = A )"
  by auto

lemma MMI_sylib: assumes A1: "φ ⟶ ψ" and
    A2: "ψ ⟷ ch"   
   shows "φ ⟶ ch"
   using assms by auto

lemma MMI_mp3an13: assumes A1: "φ" and
    A2: "ch" and
    A3: "( φ ∧ ψ ∧ ch ) ⟶ θ"   
   shows "ψ ⟶ θ"
   using assms by auto

lemma MMI_eqcomd: assumes A1: "φ ⟶ A = B"   
   shows "φ ⟶ B = A"
   using assms by auto

lemma MMI_sylan9eqr: assumes A1: "φ ⟶ A = B" and
    A2: "ψ ⟶ B = C"   
   shows "( ψ ∧ φ ) ⟶ A = C"
   using assms by auto

lemma MMI_exp32: assumes A1: "( φ ∧ ( ψ ∧ ch ) ) ⟶ θ"   
   shows "φ ⟶ ( ψ ⟶ ( ch ⟶ θ ) )"
   using assms by auto

lemma MMI_impcom: assumes A1: "φ ⟶ ( ψ ⟶ ch )"   
   shows "( ψ ∧ φ ) ⟶ ch"
   using assms by auto

lemma MMI_a1d: assumes A1: "φ ⟶ ψ"   
   shows "φ ⟶ ( ch ⟶ ψ )"
   using assms by auto

lemma MMI_r19_21aiv: assumes A1: "∀x. φ ⟶ ( x ∈ A ⟶ ψ(x) )"   
   shows "φ ⟶ ( ∀ x ∈ A . ψ(x) )"
   using assms by auto

lemma MMI_r19_22: 
   shows "( ∀ x ∈ A . ( φ(x) ⟶ ψ(x) ) ) ⟶ 
  ( ( ∃ x ∈ A . φ(x) ) ⟶ ( ∃ x ∈ A . ψ(x) ) )"
  by auto

lemma MMI_syl6: assumes A1: "φ ⟶ ( ψ ⟶ ch )" and
    A2: "ch ⟶ θ"   
   shows "φ ⟶ ( ψ ⟶ θ )"
   using assms by auto

lemma MMI_mpid: assumes A1: "φ ⟶ ch" and
    A2: "φ ⟶ ( ψ ⟶ ( ch ⟶ θ ) )"   
   shows "φ ⟶ ( ψ ⟶ θ )"
   using assms by auto

lemma MMI_eqtr3t: 
   shows "( A = C ∧ B = C ) ⟶ A = B"
  by auto

lemma MMI_syl5bi: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "θ ⟶ ψ"   
   shows "φ ⟶ ( θ ⟶ ch )"
   using assms by auto

lemma MMI_mp3an1: assumes A1: "φ" and
    A2: "( φ ∧ ψ ∧ ch ) ⟶ θ"   
   shows "( ψ ∧ ch ) ⟶ θ"
   using assms by auto

lemma MMI_rgen2: assumes A1: "∀x y. ( x ∈ A ∧ y ∈ A ) ⟶ φ(x,y)"   
   shows "∀ x ∈ A . ∀ y ∈ A . φ(x,y)"
   using assms by auto

(*************** 35-37 negeq-negeqd **************************)

lemma MMI_ax_17: shows "φ ⟶ (∀x. φ)" by simp


lemma MMI_3eqtr4g: assumes A1: "φ ⟶ A = B" and
    A2: "C = A" and
    A3: "D = B"   
   shows "φ ⟶ C = D"
   using assms by auto

(*** hbneq ***************************************************)

lemma MMI_3imtr4: assumes A1: "φ ⟶ ψ" and
    A2: "ch ⟷ φ" and
    A3: "θ ⟷ ψ"   
   shows "ch ⟶ θ"
   using assms by auto

(*lemma MMI_hbopr: assumes A1: "y ∈ A ⟶ ( ∀ x . y ∈ A )" and
    A2: "y ∈ F ⟶ ( ∀ x . y ∈ F )" and
    A3: "y ∈ B ⟶ ( ∀ x . y ∈ B )"   
   shows "y ∈ ( A F B ) ⟶ ( ∀ x . y ∈ ( A F B ) )"
   using assms by auto 
  no way to translate hopefuly we will manage to avoid using this*)

lemma MMI_eleq2i: assumes A1: "A = B"   
   shows "C ∈ A ⟷ C ∈ B"
   using assms by auto

lemma MMI_albii: assumes A1: "φ ⟷ ψ"   
   shows "( ∀ x . φ ) ⟷ ( ∀ x . ψ )"
   using assms by auto

(*************subcl-subadd **********************************)
lemma MMI_reucl: 
   shows "( ∃! x . x ∈ A ∧ φ(x) ) ⟶ ⋃ { x ∈ A . φ(x) } ∈ A"
proof
  assume A1: "∃! x . x ∈ A ∧ φ(x)"
  then obtain a where I: "a∈A"  and "φ(a)" by auto
  with A1 have "{ x ∈ A . φ(x) } = {a}" by blast
  with I show " ⋃ { x ∈ A . φ(x) } ∈ A" by simp
qed

lemma MMI_dedth2h: assumes A1: "A = if ( φ , A , C ) ⟶ ( ch ⟷ θ )" and
    A2: "B = if ( ψ , B , D ) ⟶ ( θ ⟷ τ )" and
    A3: "τ"   
   shows "( φ ∧ ψ ) ⟶ ch"
   using assms by auto

lemma MMI_eleq1d: assumes A1: "φ ⟶ A = B"   
   shows "φ ⟶ ( A ∈ C ⟷ B ∈ C )"
   using assms by auto

lemma MMI_syl5eqel: assumes A1: "φ ⟶ A ∈ B" and
    A2: "C = A"   
   shows "φ ⟶ C ∈ B"
   using assms by auto

(** a lemma in ZF that roughly corresponds to Mematamath euuni **)

lemma IML_eeuni: assumes A1: "x ∈ A" and A2: "∃! t . t ∈ A ∧ φ(t)"
  shows "φ(x) ⟷ ⋃ { x ∈ A . φ(x) } = x"
proof
  assume "φ(x)" 
  with A1 A2 show "⋃ { x ∈ A . φ(x) } = x" by auto
next assume A3: "⋃ { x ∈ A . φ(x) } = x"
  from A2 obtain y where "y∈A" and I: "φ(y)" by auto
  with A2 A3 have "x = y" by auto
  with I show "φ(x)" by simp
qed
    
lemma MMI_reuuni1: 
   shows "( x ∈ A ∧ ( ∃! x . x ∈ A ∧ φ(x) ) ) ⟶ 
  ( φ(x) ⟷ ⋃ { x ∈ A . φ(x) } = x )"
  using IML_eeuni by simp

lemma MMI_eqeq1i: assumes A1: "A = B"   
   shows "A = C ⟷ B = C"
   using assms by auto

lemma MMI_syl6rbbr: assumes A1: "∀x. φ(x) ⟶ ( ψ(x) ⟷ ch(x) )" and
    A2: "∀x. θ(x) ⟷ ch(x)"   
   shows "∀ x. φ(x) ⟶ ( θ(x) ⟷ ψ(x) )"
   using assms by auto

(*** the original version of MMI_syl6rbbr without quantifiers **********)

lemma MMI_syl6rbbrA: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "θ ⟷ ch"   
   shows "φ ⟶ ( θ ⟷ ψ )"
   using assms by auto

lemma MMI_vtoclga: assumes A1: "∀x. x = A ⟶ ( φ(x) ⟷ ψ)" and
    A2: "∀x. x ∈ B ⟶ φ(x)"
   shows "A ∈ B ⟶ ψ"
   using assms by auto

(************  subsub23 - addsubt ******************)

lemma MMI_3bitr4: assumes A1: "φ ⟷ ψ" and
    A2: "ch ⟷ φ" and
    A3: "θ ⟷ ψ"   
   shows "ch ⟷ θ"
   using assms by auto

lemma MMI_mpbii: assumes Amin: "ψ" and
    Amaj: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ch"
   using assms by auto

lemma MMI_eqid: 
   shows "A = A"
  by auto

lemma MMI_pm3_27: 
   shows "( φ ∧ ψ ) ⟶ ψ"
  by auto

lemma MMI_pm3_26: 
   shows "( φ ∧ ψ ) ⟶ φ"
  by auto

lemma MMI_ancoms: assumes A1: "( φ ∧ ψ ) ⟶ ch"   
   shows "( ψ ∧ φ ) ⟶ ch"
   using assms by auto

lemma MMI_syl3anc: assumes A1: "( φ ∧ ψ ∧ ch ) ⟶ θ" and
    A2: "τ ⟶ φ" and
    A3: "τ ⟶ ψ" and
    A4: "τ ⟶ ch"   
   shows "τ ⟶ θ"
   using assms by auto

lemma MMI_syl5eq: assumes A1: "φ ⟶ A = B" and
    A2: "C = A"   
   shows "φ ⟶ C = B"
   using assms by auto

lemma MMI_eqcomi: assumes A1: "A = B"   
   shows "B = A"
   using assms by auto

lemma MMI_3eqtr: assumes A1: "A = B" and
    A2: "B = C" and
    A3: "C = D"   
   shows "A = D"
   using assms by auto

lemma MMI_mpbir: assumes Amin: "ψ" and
    Amaj: "φ ⟷ ψ"   
   shows "φ"
   using assms by auto

lemma MMI_syl3an3: assumes A1: "( φ ∧ ψ ∧ ch ) ⟶ θ" and
    A2: "τ ⟶ ch"   
   shows "( φ ∧ ψ ∧ τ ) ⟶ θ"
   using assms by auto

lemma MMI_3eqtrd: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ B = C" and
    A3: "φ ⟶ C = D"   
   shows "φ ⟶ A = D"
   using assms by auto

lemma MMI_syl5: assumes A1: "φ ⟶ ( ψ ⟶ ch )" and
    A2: "θ ⟶ ψ"   
   shows "φ ⟶ ( θ ⟶ ch )"
   using assms by auto

lemma MMI_exp3a: assumes A1: "φ ⟶ ( ( ψ ∧ ch ) ⟶ θ )"   
   shows "φ ⟶ ( ψ ⟶ ( ch ⟶ θ ) )"
   using assms by auto

lemma MMI_com12: assumes A1: "φ ⟶ ( ψ ⟶ ch )"   
   shows "ψ ⟶ ( φ ⟶ ch )"
   using assms by auto

lemma MMI_3imp: assumes A1: "φ ⟶ ( ψ ⟶ ( ch ⟶ θ ) )"   
   shows "( φ ∧ ψ ∧ ch ) ⟶ θ"
   using assms by auto

(********* addsub12t-subidt *************)

lemma MMI_3eqtr3: assumes A1: "A = B" and
    A2: "A = C" and
    A3: "B = D"   
   shows "C = D"
   using assms by auto

lemma (in MMIsar0) MMI_opreq1i: assumes A1: "A = B"   
   shows 
  "( A \<ca> C ) = ( B \<ca> C )"
  "( A \<cs> C ) = ( B \<cs> C )"
  "( A \<cdiv> C ) = ( B \<cdiv> C )"
  "( A ⋅ C ) = ( B ⋅ C )"
   using assms by auto

lemma MMI_eqtr3: assumes A1: "A = B" and
    A2: "A = C"   
   shows "B = C"
   using assms by auto

lemma MMI_dedth: assumes A1: "A = if ( φ , A , B ) ⟶ ( ψ ⟷ ch )" and
    A2: "ch"   
   shows "φ ⟶ ψ"
   using assms by auto

lemma MMI_id: 
   shows "φ ⟶ φ"
  by auto

lemma MMI_eqtr3d: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ A = C"   
   shows "φ ⟶ B = C"
   using assms by auto

lemma MMI_sylan2: assumes A1: "( φ ∧ ψ ) ⟶ ch" and
    A2: "θ ⟶ ψ"   
   shows "( φ ∧ θ ) ⟶ ch"
   using assms by auto

lemma MMI_adantl: assumes A1: "φ ⟶ ψ"   
   shows "( ch ∧ φ ) ⟶ ψ"
   using assms by auto

lemma (in MMIsar0) MMI_opreq12: 
   shows 
  "( A = B ∧ C = D ) ⟶ ( A \<ca> C ) = ( B \<ca> D )"
  "( A = B ∧ C = D ) ⟶ ( A \<cs> C ) = ( B \<cs> D )"
  "( A = B ∧ C = D ) ⟶ ( A ⋅ C ) = ( B ⋅ D )"
  "( A = B ∧ C = D ) ⟶ ( A \<cdiv> C ) = ( B \<cdiv> D )"
  by auto

lemma MMI_anidms: assumes A1: "( φ ∧ φ ) ⟶ ψ"   
   shows "φ ⟶ ψ"
   using assms by auto

(******** subid1t-neg11 *************************)

lemma MMI_anabsan2: assumes A1: "( φ ∧ ( ψ ∧ ψ ) ) ⟶ ch"   
   shows "( φ ∧ ψ ) ⟶ ch"
   using assms by auto

lemma MMI_3simp2: 
   shows "( φ ∧ ψ ∧ ch ) ⟶ ψ"
  by auto

lemma MMI_3simp3: 
   shows "( φ ∧ ψ ∧ ch ) ⟶ ch"
  by auto

lemma MMI_sylbir: assumes A1: "ψ ⟷ φ" and
    A2: "ψ ⟶ ch"   
   shows "φ ⟶ ch"
   using assms by auto

lemma MMI_3eqtr3g: assumes A1: "φ ⟶ A = B" and
    A2: "A = C" and
    A3: "B = D"   
   shows "φ ⟶ C = D"
   using assms by auto

lemma MMI_3bitr: assumes A1: "φ ⟷ ψ" and
    A2: "ψ ⟷ ch" and
    A3: "ch ⟷ θ"   
   shows "φ ⟷ θ"
   using assms by auto

(************ negcon1-subeq0t**************)

lemma MMI_3bitr3: assumes A1: "φ ⟷ ψ" and
    A2: "φ ⟷ ch" and
    A3: "ψ ⟷ θ"   
   shows "ch ⟷ θ"
   using assms by auto

lemma MMI_eqcom: 
   shows "A = B ⟷ B = A"
  by auto

lemma MMI_syl6bb: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "ch ⟷ θ"   
   shows "φ ⟶ ( ψ ⟷ θ )"
   using assms by auto

lemma MMI_3bitr3d: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "φ ⟶ ( ψ ⟷ θ )" and
    A3: "φ ⟶ ( ch ⟷ τ )"   
   shows "φ ⟶ ( θ ⟷ τ )"
   using assms by auto

lemma MMI_syl3an2: assumes A1: "( φ ∧ ψ ∧ ch ) ⟶ θ" and
    A2: "τ ⟶ ψ"   
   shows "( φ ∧ τ ∧ ch ) ⟶ θ"
   using assms by auto

(********neg0-0re ********************)

lemma MMI_df_rex: 
   shows "( ∃ x ∈ A . φ(x) ) ⟷ ( ∃ x . ( x ∈ A ∧ φ(x) ) )"
  by auto

lemma MMI_mpbi: assumes Amin: "φ" and
    Amaj: "φ ⟷ ψ"   
   shows "ψ"
   using assms by auto

lemma MMI_mp3an12: assumes A1: "φ" and
    A2: "ψ" and
    A3: "( φ ∧ ψ ∧ ch ) ⟶ θ"   
   shows "ch ⟶ θ"
   using assms by auto

lemma MMI_syl5bb: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "θ ⟷ ψ"   
   shows "φ ⟶ ( θ ⟷ ch )"
   using assms by auto

lemma MMI_eleq1a: 
   shows "A ∈ B ⟶ ( C = A ⟶ C ∈ B )"
  by auto

lemma MMI_sylbird: assumes A1: "φ ⟶ ( ch ⟷ ψ )" and
    A2: "φ ⟶ ( ch ⟶ θ )"   
   shows "φ ⟶ ( ψ ⟶ θ )"
   using assms by auto

lemma MMI_19_23aiv: assumes A1: "∀x. φ(x) ⟶ ψ"   
   shows "( ∃ x . φ(x) ) ⟶ ψ"
   using assms by auto

lemma MMI_eqeltrrd: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ A ∈ C"   
   shows "φ ⟶ B ∈ C"
   using assms by auto

lemma MMI_syl2an: assumes A1: "( φ ∧ ψ ) ⟶ ch" and
    A2: "θ ⟶ φ" and
    A3: "τ ⟶ ψ"   
   shows "( θ ∧ τ ) ⟶ ch"
   using assms by auto

(*********** mulid2t-muladdt *********************)

lemma MMI_adantrl: assumes A1: "( φ ∧ ψ ) ⟶ ch"   
   shows "( φ ∧ ( θ ∧ ψ ) ) ⟶ ch"
   using assms by auto

lemma MMI_ad2ant2r: assumes A1: "( φ ∧ ψ ) ⟶ ch"   
   shows "( ( φ ∧ θ ) ∧ ( ψ ∧ τ ) ) ⟶ ch"
   using assms by auto

lemma MMI_adantll: assumes A1: "( φ ∧ ψ ) ⟶ ch"   
   shows "( ( θ ∧ φ ) ∧ ψ ) ⟶ ch"
   using assms by auto

lemma MMI_anandirs: assumes A1: "( ( φ ∧ ch ) ∧ ( ψ ∧ ch ) ) ⟶ τ"   
   shows "( ( φ ∧ ψ ) ∧ ch ) ⟶ τ"
   using assms by auto

lemma MMI_adantlr: assumes A1: "( φ ∧ ψ ) ⟶ ch"   
   shows "( ( φ ∧ θ ) ∧ ψ ) ⟶ ch"
   using assms by auto

lemma MMI_an42s: assumes A1: "( ( φ ∧ ψ ) ∧ ( ch ∧ θ ) ) ⟶ τ"   
   shows "( ( φ ∧ ch ) ∧ ( θ ∧ ψ ) ) ⟶ τ"
   using assms by auto

(******* muladd11t-muladd*****************************)

lemma MMI_mp3an2: assumes A1: "ψ" and
    A2: "( φ ∧ ψ ∧ ch ) ⟶ θ"   
   shows "( φ ∧ ch ) ⟶ θ"
   using assms by auto

(********** subdit-mulneg1 **************************)

lemma MMI_3simp1: 
   shows "( φ ∧ ψ ∧ ch ) ⟶ φ"
  by auto

lemma MMI_3impb: assumes A1: "( φ ∧ ( ψ ∧ ch ) ) ⟶ θ"   
   shows "( φ ∧ ψ ∧ ch ) ⟶ θ"
   using assms by auto

lemma MMI_mpbird: assumes Amin: "φ ⟶ ch" and
    Amaj: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ψ"
   using assms by auto

lemma (in MMIsar0) MMI_opreq12i: assumes A1: "A = B" and
  A2: "C = D"   
  shows 
  "( A \<ca> C ) = ( B \<ca> D )"
  "( A ⋅ C ) = ( B ⋅ D )"
  "( A \<cs> C ) = ( B \<cs> D )"
  using assms by auto

lemma MMI_3eqtr4: assumes A1: "A = B" and
  A2: "C = A" and
  A3: "D = B"   
  shows "C = D"
  using assms by auto

(*********mulneg2-negdit****************)

lemma MMI_eqtr4d: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ C = B"   
   shows "φ ⟶ A = C"
   using assms by auto

(**** negdi2t - nnncan1t ***************)

lemma MMI_3eqtr3rd: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ A = C" and
    A3: "φ ⟶ B = D"   
   shows "φ ⟶ D = C"
   using assms by auto

lemma MMI_sylanc: assumes A1: "( φ ∧ ψ ) ⟶ ch" and
    A2: "θ ⟶ φ" and
    A3: "θ ⟶ ψ"   
   shows "θ ⟶ ch"
   using assms by auto

(*** nnncan2t-pnpcan2t *******************)

lemma MMI_anim12i: assumes A1: "φ ⟶ ψ" and
    A2: "ch ⟶ θ"   
   shows "( φ ∧ ch ) ⟶ ( ψ ∧ θ )"
   using assms by auto

lemma (in MMIsar0) MMI_opreqan12d: assumes A1: "φ ⟶ A = B" and
    A2: "ψ ⟶ C = D"   
   shows 
  "( φ ∧ ψ ) ⟶ ( A \<ca> C ) = ( B \<ca> D )"
  "( φ ∧ ψ ) ⟶ ( A \<cs> C ) = ( B \<cs> D )"
  "( φ ∧ ψ ) ⟶ ( A ⋅ C ) = ( B ⋅ D )"
   using assms by auto

lemma MMI_sylanr2: assumes A1: "( φ ∧ ( ψ ∧ ch ) ) ⟶ θ" and
    A2: "τ ⟶ ch"   
   shows "( φ ∧ ( ψ ∧ τ ) ) ⟶ θ"
   using assms by auto

lemma MMI_sylanl2: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) ⟶ θ" and
    A2: "τ ⟶ ψ"   
   shows "( ( φ ∧ τ ) ∧ ch ) ⟶ θ"
   using assms by auto

lemma MMI_ancom2s: assumes A1: "( φ ∧ ( ψ ∧ ch ) ) ⟶ θ"   
   shows "( φ ∧ ( ch ∧ ψ ) ) ⟶ θ"
   using assms by auto

lemma MMI_anandis: assumes A1: "( ( φ ∧ ψ ) ∧ ( φ ∧ ch ) ) ⟶ τ"   
   shows "( φ ∧ ( ψ ∧ ch ) ) ⟶ τ"
   using assms by auto

lemma MMI_sylan9eq: assumes A1: "φ ⟶ A = B" and
    A2: "ψ ⟶ B = C"   
   shows "( φ ∧ ψ ) ⟶ A = C"
   using assms by auto

(******pnncant-mul0ort**********************)

lemma MMI_keephyp: assumes A1: "A = if ( φ , A , B ) ⟶ ( ψ ⟷ θ )" and
    A2: "B = if ( φ , A , B ) ⟶ ( ch ⟷ θ )" and
    A3: "ψ" and
    A4: "ch"   
   shows "θ"
proof -
  { assume "φ"
    with A1 A3 have "θ" by simp }
  moreover
  { assume "¬φ"
    with A2 A4 have "θ" by simp }
  ultimately show "θ" by auto
qed

lemma MMI_eleq1: 
   shows "A = B ⟶ ( A ∈ C ⟷ B ∈ C )"
  by auto

lemma MMI_pm4_2i: 
   shows "φ ⟶ ( ψ ⟷ ψ )"
  by auto

lemma MMI_3anbi123d: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "φ ⟶ ( θ ⟷ τ )" and
    A3: "φ ⟶ ( η ⟷ ζ )"   
   shows "φ ⟶ ( ( ψ ∧ θ ∧ η ) ⟷ ( ch ∧ τ ∧ ζ ) )"
   using assms by auto

lemma MMI_imbi12d: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "φ ⟶ ( θ ⟷ τ )"   
   shows "φ ⟶ ( ( ψ ⟶ θ ) ⟷ ( ch ⟶ τ ) )"
   using assms by auto

lemma MMI_bitrd: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "φ ⟶ ( ch ⟷ θ )"   
   shows "φ ⟶ ( ψ ⟷ θ )"
   using assms by auto

lemma MMI_df_ne: 
   shows "( A ≠ B ⟷ ¬ ( A = B ) )"
  by auto

lemma MMI_3pm3_2i: assumes A1: "φ" and
    A2: "ψ" and
    A3: "ch"   
   shows "φ ∧ ψ ∧ ch"
   using assms by auto

lemma MMI_eqeq2i: assumes A1: "A = B"   
   shows "C = A ⟷ C = B"
   using assms by auto

lemma MMI_syl5bbr: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "ψ ⟷ θ"   
   shows "φ ⟶ ( θ ⟷ ch )"
   using assms by auto

lemma MMI_biimpd: assumes A1: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ( ψ ⟶ ch )"
   using assms by auto

lemma MMI_orrd: assumes A1: "φ ⟶ ( ¬ ( ψ ) ⟶ ch )"   
   shows "φ ⟶ ( ψ ∨ ch )"
   using assms by auto

lemma MMI_jaoi: assumes A1: "φ ⟶ ψ" and
    A2: "ch ⟶ ψ"   
   shows "( φ ∨ ch ) ⟶ ψ"
   using assms by auto

lemma MMI_oridm: 
   shows "( φ ∨ φ ) ⟷ φ"
  by auto

lemma MMI_orbi1d: assumes A1: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ( ( ψ ∨ θ ) ⟷ ( ch ∨ θ ) )"
   using assms by auto

lemma MMI_orbi2d: assumes A1: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ( ( θ ∨ ψ ) ⟷ ( θ ∨ ch ) )"
   using assms by auto

(********* muln0bt-receu ******************)

lemma MMI_3bitr4g: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "θ ⟷ ψ" and
    A3: "τ ⟷ ch"   
   shows "φ ⟶ ( θ ⟷ τ )"
   using assms by auto

lemma MMI_negbid: assumes A1: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ( ¬ ( ψ ) ⟷ ¬ ( ch ) )"
   using assms by auto

lemma MMI_ioran: 
   shows "¬ ( ( φ ∨ ψ ) ) ⟷ 
 ( ¬ ( φ ) ∧ ¬ ( ψ ) )"
  by auto

lemma MMI_syl6rbb: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "ch ⟷ θ"   
   shows "φ ⟶ ( θ ⟷ ψ )"
   using assms by auto

lemma MMI_anbi12i: assumes A1: "φ ⟷ ψ" and
    A2: "ch ⟷ θ"   
   shows "( φ ∧ ch ) ⟷ ( ψ ∧ θ )"
   using assms by auto

(*******divmul-divclz ******************)


lemma MMI_keepel: assumes A1: "A ∈ C" and
    A2: "B ∈ C"   
   shows "if ( φ , A , B ) ∈ C"
   using assms by auto

lemma MMI_imbi2d: assumes A1: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ( ( θ ⟶ ψ ) ⟷ ( θ ⟶ ch ) )"
   using assms by auto

(** this was recognized as known , although not proven yet**)

lemma MMI_eqeltr: assumes "A = B" and "B ∈ C"
  shows "A ∈ C" using assms by auto

(*****divclt-divcan2t*******************)

lemma MMI_3impia: assumes A1: "( φ ∧ ψ ) ⟶ ( ch ⟶ θ )"   
   shows "( φ ∧ ψ ∧ ch ) ⟶ θ"
   using assms by auto

(********* divne0bt-divrecz************)

lemma MMI_eqneqd: assumes A1: "φ ⟶ ( A = B ⟷ C = D )"   
   shows "φ ⟶ ( A ≠ B ⟷ C ≠ D )"
   using assms by auto

lemma MMI_3ad2ant2: assumes A1: "φ ⟶ ch"   
   shows "( ψ ∧ φ ∧ θ ) ⟶ ch"
   using assms by auto

lemma MMI_mp3anl3: assumes A1: "ch" and
    A2: "( ( φ ∧ ψ ∧ ch ) ∧ θ ) ⟶ τ"   
   shows "( ( φ ∧ ψ ) ∧ θ ) ⟶ τ"
   using assms by auto

lemma MMI_bitr4d: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "φ ⟶ ( θ ⟷ ch )"   
   shows "φ ⟶ ( ψ ⟷ θ )"
   using assms by auto

lemma MMI_neeq1d: assumes A1: "φ ⟶ A = B"   
   shows "φ ⟶ ( A ≠ C ⟷ B ≠ C )"
   using assms by auto

(*******divrect-div23***********************)

lemma MMI_3anim123i: assumes A1: "φ ⟶ ψ" and
    A2: "ch ⟶ θ" and
    A3: "τ ⟶ η"   
   shows "( φ ∧ ch ∧ τ ) ⟶ ( ψ ∧ θ ∧ η )"
   using assms by auto

lemma MMI_3exp: assumes A1: "( φ ∧ ψ ∧ ch ) ⟶ θ"   
   shows "φ ⟶ ( ψ ⟶ ( ch ⟶ θ ) )"
   using assms by auto

lemma MMI_exp4a: assumes A1: "φ ⟶ ( ψ ⟶ ( ( ch ∧ θ ) ⟶ τ ) )"   
   shows "φ ⟶ ( ψ ⟶ ( ch ⟶ ( θ ⟶ τ ) ) )"
   using assms by auto

lemma MMI_3imp1: assumes A1: "φ ⟶ ( ψ ⟶ ( ch ⟶ ( θ ⟶ τ ) ) )"   
   shows "( ( φ ∧ ψ ∧ ch ) ∧ θ ) ⟶ τ"
   using assms by auto

lemma MMI_anim1i: assumes A1: "φ ⟶ ψ"   
   shows "( φ ∧ ch ) ⟶ ( ψ ∧ ch )"
   using assms by auto

lemma MMI_3adantl1: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) ⟶ θ"   
   shows "( ( τ ∧ φ ∧ ψ ) ∧ ch ) ⟶ θ"
   using assms by auto

lemma MMI_3adantl2: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) ⟶ θ"   
   shows "( ( φ ∧ τ ∧ ψ ) ∧ ch ) ⟶ θ"
   using assms by auto

lemma MMI_3comr: assumes A1: "( φ ∧ ψ ∧ ch ) ⟶ θ"   
   shows "( ch ∧ φ ∧ ψ ) ⟶ θ"
   using assms by auto

(***********divdirz-div11t*************************)

lemma MMI_bitr3: assumes A1: "ψ ⟷ φ" and
    A2: "ψ ⟷ ch"   
   shows "φ ⟷ ch"
   using assms by auto

lemma MMI_anbi12d: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "φ ⟶ ( θ ⟷ τ )"   
   shows "φ ⟶ ( ( ψ ∧ θ ) ⟷ ( ch ∧ τ ) )"
   using assms by auto

lemma MMI_pm3_26i: assumes A1: "φ ∧ ψ"   
   shows "φ"
   using assms by auto

lemma MMI_pm3_27i: assumes A1: "φ ∧ ψ"   
   shows "ψ"
   using assms by auto

(*********dividt-divsubdirt************************)

lemma MMI_anabsan: assumes A1: "( ( φ ∧ φ ) ∧ ψ ) ⟶ ch"   
   shows "( φ ∧ ψ ) ⟶ ch"
   using assms by auto

lemma MMI_3eqtr4rd: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ C = A" and
    A3: "φ ⟶ D = B"   
   shows "φ ⟶ D = C"
   using assms by auto

lemma MMI_syl3an1: assumes A1: "( φ ∧ ψ ∧ ch ) ⟶ θ" and
    A2: "τ ⟶ φ"   
   shows "( τ ∧ ψ ∧ ch ) ⟶ θ"
   using assms by auto

lemma MMI_syl3anl2: assumes A1: "( ( φ ∧ ψ ∧ ch ) ∧ θ ) ⟶ τ" and
    A2: "η ⟶ ψ"   
   shows "( ( φ ∧ η ∧ ch ) ∧ θ ) ⟶ τ"
   using assms by auto

(******* recrect-divmuldiv ****************)


lemma MMI_jca: assumes A1: "φ ⟶ ψ" and
    A2: "φ ⟶ ch"   
   shows "φ ⟶ ( ψ ∧ ch )"
   using assms by auto

lemma MMI_3ad2ant3: assumes A1: "φ ⟶ ch"   
   shows "( ψ ∧ θ ∧ φ ) ⟶ ch"
   using assms by auto

lemma MMI_anim2i: assumes A1: "φ ⟶ ψ"   
   shows "( ch ∧ φ ) ⟶ ( ch ∧ ψ )"
   using assms by auto

lemma MMI_ancom: 
   shows "( φ ∧ ψ ) ⟷ ( ψ ∧ φ )"
  by auto

lemma MMI_anbi1i: assumes Aaa: "φ ⟷ ψ"   
   shows "( φ ∧ ch ) ⟷ ( ψ ∧ ch )"
   using assms by auto

lemma MMI_an42: 
   shows "( ( φ ∧ ψ ) ∧ ( ch ∧ θ ) ) ⟷ 
 ( ( φ ∧ ch ) ∧ ( θ ∧ ψ ) )"
  by auto

lemma MMI_sylanb: assumes A1: "( φ ∧ ψ ) ⟶ ch" and
    A2: "θ ⟷ φ"   
   shows "( θ ∧ ψ ) ⟶ ch"
   using assms by auto

lemma MMI_an4: 
   shows "( ( φ ∧ ψ ) ∧ ( ch ∧ θ ) ) ⟷ 
 ( ( φ ∧ ch ) ∧ ( ψ ∧ θ ) )"
  by auto

lemma MMI_syl2anb: assumes A1: "( φ ∧ ψ ) ⟶ ch" and
    A2: "θ ⟷ φ" and
    A3: "τ ⟷ ψ"   
   shows "( θ ∧ τ ) ⟶ ch"
   using assms by auto

lemma MMI_eqtr2d: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ B = C"   
   shows "φ ⟶ C = A"
   using assms by auto

lemma MMI_sylbid: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "φ ⟶ ( ch ⟶ θ )"   
   shows "φ ⟶ ( ψ ⟶ θ )"
   using assms by auto

lemma MMI_sylanl1: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) ⟶ θ" and
    A2: "τ ⟶ φ"   
   shows "( ( τ ∧ ψ ) ∧ ch ) ⟶ θ"
   using assms by auto

lemma MMI_sylan2b: assumes A1: "( φ ∧ ψ ) ⟶ ch" and
    A2: "θ ⟷ ψ"   
   shows "( φ ∧ θ ) ⟶ ch"
   using assms by auto

lemma MMI_pm3_22: 
   shows "( φ ∧ ψ ) ⟶ ( ψ ∧ φ )"
  by auto

lemma MMI_ancli: assumes A1: "φ ⟶ ψ"   
   shows "φ ⟶ ( φ ∧ ψ )"
   using assms by auto

lemma MMI_ad2antlr: assumes A1: "φ ⟶ ψ"   
   shows "( ( ch ∧ φ ) ∧ θ ) ⟶ ψ"
   using assms by auto

lemma MMI_biimpa: assumes A1: "φ ⟶ ( ψ ⟷ ch )"   
   shows "( φ ∧ ψ ) ⟶ ch"
   using assms by auto

lemma MMI_sylan2i: assumes A1: "φ ⟶ ( ( ψ ∧ ch ) ⟶ θ )" and
    A2: "τ ⟶ ch"   
   shows "φ ⟶ ( ( ψ ∧ τ ) ⟶ θ )"
   using assms by auto

lemma MMI_3jca: assumes A1: "φ ⟶ ψ" and
    A2: "φ ⟶ ch" and
    A3: "φ ⟶ θ"   
   shows "φ ⟶ ( ψ ∧ ch ∧ θ )"
   using assms by auto

lemma MMI_com34: assumes A1: "φ ⟶ ( ψ ⟶ ( ch ⟶ ( θ ⟶ τ ) ) )"   
   shows "φ ⟶ ( ψ ⟶ ( θ ⟶ ( ch ⟶ τ ) ) )"
   using assms by auto

lemma MMI_imp43: assumes A1: "φ ⟶ ( ψ ⟶ ( ch ⟶ ( θ ⟶ τ ) ) )"   
   shows "( ( φ ∧ ψ ) ∧ ( ch ∧ θ ) ) ⟶ τ"
   using assms by auto

lemma MMI_3anass: 
   shows "( φ ∧ ψ ∧ ch ) ⟷ ( φ ∧ ( ψ ∧ ch ) )"
  by auto

(************ divmul13-redivclt*************)

lemma MMI_3eqtr4r: assumes A1: "A = B" and
    A2: "C = A" and
    A3: "D = B"   
   shows "D = C"
   using assms by auto

lemma MMI_jctl: assumes A1: "ψ"   
   shows "φ ⟶ ( ψ ∧ φ )"
   using assms by auto

lemma MMI_sylibr: assumes A1: "φ ⟶ ψ" and
    A2: "ch ⟷ ψ"   
   shows "φ ⟶ ch"
   using assms by auto

lemma MMI_mpanl1: assumes A1: "φ" and
    A2: "( ( φ ∧ ψ ) ∧ ch ) ⟶ θ"   
   shows "( ψ ∧ ch ) ⟶ θ"
   using assms by auto

lemma MMI_a1i: assumes A1: "φ"   
   shows "ψ ⟶ φ"
   using assms by auto

lemma (in MMIsar0) MMI_opreqan12rd: assumes A1: "φ ⟶ A = B" and
    A2: "ψ ⟶ C = D"   
   shows 
  "( ψ ∧ φ ) ⟶ ( A \<ca> C ) = ( B \<ca> D )"
  "( ψ ∧ φ ) ⟶ ( A ⋅ C ) = ( B ⋅ D )"
  "( ψ ∧ φ ) ⟶ ( A \<cs> C ) = ( B \<cs> D )"
  "( ψ ∧ φ ) ⟶ ( A \<cdiv> C ) = ( B \<cdiv> D )"
   using assms by auto

lemma MMI_3adantl3: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) ⟶ θ"   
   shows "( ( φ ∧ ψ ∧ τ ) ∧ ch ) ⟶ θ"
   using assms by auto

lemma MMI_sylbi: assumes A1: "φ ⟷ ψ" and
    A2: "ψ ⟶ ch"   
   shows "φ ⟶ ch"
   using assms by auto

(*******pnfnre,minfnre*******************)

lemma MMI_eirr: 
   shows "¬ ( A ∈ A )"
  by (rule mem_not_refl)

lemma MMI_eleq1i: assumes A1: "A = B"   
   shows "A ∈ C ⟷ B ∈ C"
   using assms by auto

lemma MMI_mtbir: assumes A1: "¬ ( ψ )" and
    A2: "φ ⟷ ψ"   
   shows "¬ ( φ )"
   using assms by auto

lemma MMI_mto: assumes A1: "¬ ( ψ )" and
    A2: "φ ⟶ ψ"   
   shows "¬ ( φ )"
   using assms by auto

lemma MMI_df_nel: 
   shows "( A ∉ B ⟷ ¬ ( A ∈ B ) )"
  by auto

lemma MMI_snid: assumes A1: "A isASet"   
   shows "A ∈ { A }"
   using assms by auto

lemma MMI_en2lp: 
   shows "¬ ( A ∈ B ∧ B ∈ A )"
proof
  assume A1: "A ∈ B ∧ B ∈ A"
  then have "A ∈ B" by simp
  moreover
  { assume "¬ (¬ ( A ∈ B ∧ B ∈ A ))"
    then have "B∈A" by auto}
  ultimately have "¬( A ∈ B ∧ B ∈ A )"
    by (rule mem_asym)
  with A1 show False by simp
qed

lemma MMI_imnan: 
   shows "( φ ⟶ ¬ ( ψ ) ) ⟷ ¬ ( ( φ ∧ ψ ) )"
  by auto

(****ressxr-ltxrltt*******************************)

lemma MMI_sseqtr4: assumes A1: "A ⊆ B" and
    A2: "C = B"   
   shows "A ⊆ C"
   using assms by auto

lemma MMI_ssun1: 
   shows "A ⊆ ( A ∪ B )"
  by auto

lemma MMI_ibar: 
   shows "φ ⟶ ( ψ ⟷ ( φ ∧ ψ ) )"
  by auto

lemma MMI_mtbiri: assumes Amin: "¬ ( ch )" and
    Amaj: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ¬ ( ψ )"
   using assms by auto

lemma MMI_con2i: assumes Aa: "φ ⟶ ¬ ( ψ )"   
   shows "ψ ⟶ ¬ ( φ )"
   using assms by auto

lemma MMI_intnand: assumes A1: "φ ⟶ ¬ ( ψ )"   
   shows "φ ⟶ ¬ ( ( ch ∧ ψ ) )"
   using assms by auto

lemma MMI_intnanrd: assumes A1: "φ ⟶ ¬ ( ψ )"   
   shows "φ ⟶ ¬ ( ( ψ ∧ ch ) )"
   using assms by auto

lemma MMI_biorf: 
   shows "¬ ( φ ) ⟶ ( ψ ⟷ ( φ ∨ ψ ) )"
  by auto

lemma MMI_bitr2d: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "φ ⟶ ( ch ⟷ θ )"   
   shows "φ ⟶ ( θ ⟷ ψ )"
   using assms by auto

lemma MMI_orass: 
   shows "( ( φ ∨ ψ ) ∨ ch ) ⟷ ( φ ∨ ( ψ ∨ ch ) )"
  by auto

lemma MMI_orcom: 
   shows "( φ ∨ ψ ) ⟷ ( ψ ∨ φ )"
  by auto

(************** axlttri,axlttrn****************)
(* note these are not really axioms of 
    complex numbers, just extensions of
    pre_axlttri and pre_axlttrn that are assumed
    in the context.                           
*)

lemma MMI_3bitr4d: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "φ ⟶ ( θ ⟷ ψ )" and
    A3: "φ ⟶ ( τ ⟷ ch )"   
   shows "φ ⟶ ( θ ⟷ τ )"
   using assms by auto

lemma MMI_3imtr4d: assumes A1: "φ ⟶ ( ψ ⟶ ch )" and
    A2: "φ ⟶ ( θ ⟷ ψ )" and
    A3: "φ ⟶ ( τ ⟷ ch )"   
   shows "φ ⟶ ( θ ⟶ τ )"
   using assms by auto

(**********axltadd-ltnlet*************************)

lemma MMI_3impdi: assumes A1: "( ( φ ∧ ψ ) ∧ ( φ ∧ ch ) ) ⟶ θ"   
   shows "( φ ∧ ψ ∧ ch ) ⟶ θ"
   using assms by auto

lemma MMI_bi2anan9: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "θ ⟶ ( τ ⟷ η )"   
   shows "( φ ∧ θ ) ⟶ ( ( ψ ∧ τ ) ⟷ ( ch ∧ η ) )"
   using assms by auto

lemma MMI_ssel2: 
   shows "( ( A ⊆ B ∧ C ∈ A ) ⟶ C ∈ B )"
  by auto

lemma MMI_an1rs: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) ⟶ θ"   
   shows "( ( φ ∧ ch ) ∧ ψ ) ⟶ θ"
   using assms by auto

(*lemma MMI_ralbidva_original: 
     assumes A1: "( φ ∧ x ∈ A ) ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶  ( ( ∀ x ∈ A . ψ ) ⟷ ( ∀ x ∈ A . ch ) )"
   using assms by auto;*)

lemma MMI_ralbidva: assumes A1: "∀x. ( φ ∧ x ∈ A ) ⟶ ( ψ(x) ⟷ ch(x) )"   
   shows "φ ⟶  ( ( ∀ x ∈ A . ψ(x) ) ⟷ ( ∀ x ∈ A . ch(x) ) )"
   using assms by auto

lemma MMI_rexbidva: assumes A1: "∀x. ( φ ∧ x ∈ A ) ⟶ ( ψ(x) ⟷ ch(x) )"   
   shows "φ ⟶  ( ( ∃ x ∈ A . ψ(x) ) ⟷ ( ∃ x ∈ A . ch(x) ) )"
   using assms by auto

lemma MMI_con2bid: assumes A1: "φ ⟶ ( ψ ⟷ ¬ ( ch ) )"   
   shows "φ ⟶ ( ch ⟷ ¬ ( ψ ) )"
   using assms by auto

(********ltso***************************)
lemma MMI_so: assumes 
  A1: "∀x y z. ( x ∈ A ∧ y ∈ A ∧ z ∈ A ) ⟶   
  ( ( ⟨x,y⟩ ∈ R ⟷ ¬ ( ( x = y ∨ ⟨y, x⟩ ∈ R ) ) ) ∧ 
  ( ( ⟨x, y⟩ ∈ R  ∧ ⟨y, z⟩ ∈ R ) ⟶ ⟨x, z⟩ ∈ R ) )"   
  shows "R Orders A"
  using assms StrictOrder_def by auto

(***********lttri2t-letri3t**********************)

lemma MMI_con1bid: assumes A1: "φ ⟶ ( ¬ ( ψ ) ⟷ ch )"   
   shows "φ ⟶ ( ¬ ( ch ) ⟷ ψ )"
   using assms by auto

lemma MMI_sotrieq: 
  shows "( (R Orders A) ∧ ( B ∈ A ∧ C ∈ A ) ) ⟶   
  ( B = C ⟷ ¬ ( ( ⟨B,C⟩ ∈ R ∨ ⟨C, B⟩ ∈ R ) ) )"
proof -
  { assume A1: "R Orders A"  and A2: "B ∈ A ∧ C ∈ A" 
    from A1 have "∀x y z. (x∈A ∧ y∈A ∧ z∈A) ⟶ 
      (⟨x,y⟩ ∈ R ⟷ ¬(x=y ∨ ⟨y,x⟩ ∈ R)) ∧ 
      (⟨x,y⟩ ∈ R ∧ ⟨y,z⟩ ∈ R ⟶ ⟨x,z⟩ ∈ R)"
      by (unfold StrictOrder_def)
    then have 
      "∀x y. x∈A ∧ y∈A ⟶ (⟨x,y⟩ ∈ R ⟷ ¬(x=y ∨ ⟨y,x⟩ ∈ R))"
      by auto
    with A2 have I: "⟨B,C⟩ ∈ R ⟷ ¬(B=C ∨ ⟨C,B⟩ ∈ R)"
      by blast
    then have "B = C ⟷ ¬ ( ⟨B,C⟩ ∈ R ∨ ⟨C, B⟩ ∈ R )"
      by auto
  } then show "( (R Orders A) ∧ ( B ∈ A ∧ C ∈ A ) ) ⟶   
      ( B = C ⟷ ¬ ( ( ⟨B,C⟩ ∈ R ∨ ⟨C, B⟩ ∈ R ) ) )" by simp
qed

lemma MMI_bicomd: assumes A1: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ( ch ⟷ ψ )"
   using assms by auto

lemma MMI_sotrieq2: 
  shows "( R Orders A ∧ ( B ∈ A ∧ C ∈ A ) ) ⟶   
  ( B =  C ⟷ ( ¬ ( ⟨B, C⟩ ∈ R ) ∧ ¬ ( ⟨C, B⟩ ∈ R ) ) )"
  using  MMI_sotrieq by auto

lemma MMI_orc: 
   shows "φ ⟶ ( φ ∨ ψ )"
  by auto

lemma MMI_syl6bbr: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "θ ⟷ ch"   
   shows "φ ⟶ ( ψ ⟷ θ )"
   using assms by auto

(***********leloet-lelttrd*****************)

lemma MMI_orbi1i: assumes A1: "φ ⟷ ψ"   
   shows "( φ ∨ ch ) ⟷ ( ψ ∨ ch )"
   using assms by auto

lemma MMI_syl5rbbr: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "ψ ⟷ θ"   
   shows "φ ⟶ ( ch ⟷ θ )"
   using assms by auto

lemma MMI_anbi2d: assumes A1: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ( ( θ ∧ ψ ) ⟷ ( θ ∧ ch ) )"
   using assms by auto

lemma MMI_ord: assumes A1: "φ ⟶ ( ψ ∨ ch )"   
   shows "φ ⟶ ( ¬ ( ψ ) ⟶ ch )"
   using assms by auto

lemma MMI_impbid: assumes A1: "φ ⟶ ( ψ ⟶ ch )" and
    A2: "φ ⟶ ( ch ⟶ ψ )"   
   shows "φ ⟶ ( ψ ⟷ ch )"
   using assms by blast

lemma MMI_jcad: assumes A1: "φ ⟶ ( ψ ⟶ ch )" and
    A2: "φ ⟶ ( ψ ⟶ θ )"   
   shows "φ ⟶ ( ψ ⟶ ( ch ∧ θ ) )"
   using assms by auto

lemma MMI_ax_1: 
   shows "φ ⟶ ( ψ ⟶ φ )"
  by auto

lemma MMI_pm2_24: 
   shows "φ ⟶ ( ¬ ( φ ) ⟶ ψ )"
  by auto

lemma MMI_imp3a: assumes A1: "φ ⟶ ( ψ ⟶ ( ch ⟶ θ ) )"   
   shows "φ ⟶ ( ( ψ ∧ ch ) ⟶ θ )"
   using assms by auto

lemma (in MMIsar0) MMI_breq1: 
   shows 
  "A = B ⟶ ( A \<lsq> C ⟷ B \<lsq> C )"
  "A = B ⟶ ( A \<ls> C ⟷ B \<ls> C )"
  by auto

lemma MMI_biimprd: assumes A1: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ( ch ⟶ ψ )"
   using assms by auto

lemma MMI_jaod: assumes A1: "φ ⟶ ( ψ ⟶ ch )" and
    A2: "φ ⟶ ( θ ⟶ ch )"   
   shows "φ ⟶ ( ( ψ ∨ θ ) ⟶ ch )"
   using assms by auto

lemma MMI_com23: assumes A1: "φ ⟶ ( ψ ⟶ ( ch ⟶ θ ) )"   
   shows "φ ⟶ ( ch ⟶ ( ψ ⟶ θ ) )"
   using assms by auto

lemma (in MMIsar0) MMI_breq2: 
   shows 
  "A = B ⟶ ( C \<lsq> A ⟷ C \<lsq> B )"
  "A = B ⟶ ( C \<ls> A ⟷ C \<ls> B )"
  by auto

lemma MMI_syld: assumes A1: "φ ⟶ ( ψ ⟶ ch )" and
    A2: "φ ⟶ ( ch ⟶ θ )"   
   shows "φ ⟶ ( ψ ⟶ θ )"
   using assms by auto

lemma MMI_biimpcd: assumes A1: "φ ⟶ ( ψ ⟷ ch )"   
   shows "ψ ⟶ ( φ ⟶ ch )"
   using assms by auto

lemma MMI_mp2and: assumes A1: "φ ⟶ ψ" and
    A2: "φ ⟶ ch" and
    A3: "φ ⟶ ( ( ψ ∧ ch ) ⟶ θ )"   
   shows "φ ⟶ θ"
   using assms by auto

(**********ltletrd-renemnft*********************)

lemma MMI_sonr: 
   shows "( R Orders A ∧ B ∈ A ) ⟶ ¬ ( ⟨B,B⟩ ∈ R )"
  unfolding StrictOrder_def by auto

lemma MMI_orri: assumes A1: "¬ ( φ ) ⟶ ψ"   
   shows "φ ∨ ψ"
   using assms by auto

lemma MMI_mpbiri: assumes Amin: "ch" and
    Amaj: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ψ"
   using assms by auto

lemma MMI_pm2_46: 
   shows "¬ ( ( φ ∨ ψ ) ) ⟶ ¬ ( ψ )"
  by auto

lemma MMI_elun: 
   shows "A ∈ ( B ∪ C ) ⟷ ( A ∈ B ∨ A ∈ C )"
  by auto

lemma (in MMIsar0) MMI_pnfxr: 
   shows "\<cpnf> ∈ ℝ⇧*"
  using cxr_def by simp

lemma MMI_elisseti: assumes A1: "A ∈ B"   
   shows "A isASet"
   using assms by auto

lemma (in MMIsar0) MMI_mnfxr: 
   shows "\<cmnf> ∈ ℝ⇧*"
  using  cxr_def by simp

lemma MMI_elpr2: assumes A1: "B isASet" and
    A2: "C isASet"   
   shows "A ∈ { B , C } ⟷ ( A = B ∨ A = C )"
   using assms by auto

lemma MMI_orbi2i: assumes A1: "φ ⟷ ψ"   
   shows "( ch ∨ φ ) ⟷ ( ch ∨ ψ )"
   using assms by auto

lemma MMI_3orass: 
   shows "( φ ∨ ψ ∨ ch ) ⟷ ( φ ∨ ( ψ ∨ ch ) )"
  by auto

lemma MMI_bitr4: assumes A1: "φ ⟷ ψ" and
    A2: "ch ⟷ ψ"   
   shows "φ ⟷ ch"
   using assms by auto

lemma MMI_eleq2: 
   shows "A = B ⟶ ( C ∈ A ⟷ C ∈ B )"
  by auto

lemma MMI_nelneq: 
   shows "( A ∈ C ∧ ¬ ( B ∈ C ) ) ⟶ ¬ ( A = B )"
  by auto

(************ renfdisj - pnfget *********************)

lemma MMI_df_pr: 
   shows "{ A , B } = ( { A } ∪ { B } )"
  by auto

lemma MMI_ineq2i: assumes A1: "A = B"   
   shows "( C ∩ A ) = ( C ∩ B )"
   using assms by auto

lemma MMI_mt2: assumes A1: "ψ" and
    A2: "φ ⟶ ¬ ( ψ )"   
   shows "¬ ( φ )"
   using assms by auto

lemma MMI_disjsn: 
   shows "( A ∩ { B } ) = 0 ⟷ ¬ ( B ∈ A )"
  by auto

lemma MMI_undisj2: 
   shows "( ( A ∩ B ) =   
 0 ∧ ( A ∩ C ) =   
 0 ) ⟷ ( A ∩ ( B ∪ C ) ) = 0"
  by auto

lemma MMI_disjssun: 
   shows "( ( A ∩ B ) =  0 ⟶ ( A ⊆ ( B ∪ C ) ⟷ A ⊆ C ) )"
  by auto

lemma MMI_uncom: 
   shows "( A ∪ B ) = ( B ∪ A )"
  by auto

lemma MMI_sseq2i: assumes A1: "A = B"   
   shows "( C ⊆ A ⟷ C ⊆ B )"
   using assms by auto

lemma MMI_disj: 
   shows "( A ∩ B ) =   
 0 ⟷ ( ∀ x ∈ A . ¬ ( x ∈ B ) )"
  by auto

lemma MMI_syl5ibr: assumes A1: "φ ⟶ ( ψ ⟶ ch )" and
    A2: "ψ ⟷ θ"   
   shows "φ ⟶ ( θ ⟶ ch )"
   using assms by auto

lemma MMI_con3d: assumes A1: "φ ⟶ ( ψ ⟶ ch )"   
   shows "φ ⟶ ( ¬ ( ch ) ⟶ ¬ ( ψ ) )"
   using assms by auto

(* original lemma MMI_dfrex2: 
   shows "( ∃ x ∈ A . φ ) ⟷  ¬ ( ( ∀ x ∈ A . ¬ ( φ ) ) )"
  by auto*)

lemma MMI_dfrex2: 
  shows "( ∃ x ∈ A . φ(x) ) ⟷  ¬ ( ( ∀ x ∈ A . ¬ φ(x) ) )"
  by auto

lemma MMI_visset: 
   shows "x isASet"
  by auto

lemma MMI_elpr: assumes A1: "A isASet"   
   shows "A ∈ { B , C } ⟷ ( A = B ∨ A = C )"
   using assms by auto

lemma MMI_rexbii: assumes A1: "∀x. φ(x) ⟷ ψ(x)"   
   shows "( ∃ x ∈ A . φ(x) ) ⟷ ( ∃ x ∈ A . ψ(x) )"
   using assms by auto

lemma MMI_r19_43: 
   shows "( ∃ x ∈ A . ( φ(x) ∨ ψ(x) ) ) ⟷   
 ( ( ∃ x ∈ A . φ(x) ∨ ( ∃ x ∈ A . ψ(x) ) ) )"
  by auto

lemma MMI_exancom: 
   shows "( ∃ x . ( φ(x) ∧ ψ(x) ) ) ⟷   
 ( ∃ x . ( ψ(x) ∧ φ(x) ) )"
  by auto

lemma MMI_ceqsexv: assumes A1: "A isASet" and
    A2: "∀x. x = A ⟶ ( φ(x) ⟷ ψ(x) )"   
   shows "( ∃ x . ( x = A ∧ φ(x) ) ) ⟷ ψ(A)"
   using assms by auto

lemma MMI_orbi12i_orig: assumes A1: "φ ⟷ ψ" and
    A2: "ch ⟷ θ"   
   shows "( φ ∨ ch ) ⟷ ( ψ ∨ θ )"
   using assms by auto

lemma MMI_orbi12i: assumes A1: "(∃x. φ(x)) ⟷ ψ" and
    A2: "(∃x. ch(x)) ⟷ θ"   
   shows "( ∃x. φ(x) ) ∨ (∃x. ch(x) ) ⟷ ( ψ ∨ θ )"
   using assms by auto

lemma MMI_syl6ib: assumes A1: "φ ⟶ ( ψ ⟶ ch )" and
    A2: "ch ⟷ θ"   
   shows "φ ⟶ ( ψ ⟶ θ )"
   using assms by auto

lemma MMI_intnan: assumes A1: "¬ ( φ )"   
   shows "¬ ( ( ψ ∧ φ ) )"
   using assms by auto

lemma MMI_intnanr: assumes A1: "¬ ( φ )"   
   shows "¬ ( ( φ ∧ ψ ) )"
   using assms by auto

lemma MMI_pm3_2ni: assumes A1: "¬ ( φ )" and
    A2: "¬ ( ψ )"   
   shows "¬ ( ( φ ∨ ψ ) )"
   using assms by auto

lemma (in MMIsar0) MMI_breq12: 
   shows 
  "( A = B ∧ C = D ) ⟶ ( A \<ls> C ⟷ B \<ls> D )"
  "( A = B ∧ C = D ) ⟶ ( A \<lsq> C ⟷ B \<lsq> D )"
  by auto

lemma MMI_necom: 
   shows "A ≠ B ⟷ B ≠ A"
  by auto

lemma MMI_3jaoi: assumes A1: "φ ⟶ ψ" and
    A2: "ch ⟶ ψ" and
    A3: "θ ⟶ ψ"   
   shows "( φ ∨ ch ∨ θ ) ⟶ ψ"
   using assms by auto

lemma MMI_jctr: assumes A1: "ψ"   
   shows "φ ⟶ ( φ ∧ ψ )"
   using assms by auto

lemma MMI_olc: 
   shows "φ ⟶ ( ψ ∨ φ )"
  by auto

lemma MMI_3syl: assumes A1: "φ ⟶ ψ" and
    A2: "ψ ⟶ ch" and
    A3: "ch ⟶ θ"   
   shows "φ ⟶ θ"
   using assms by auto

(************** mnflet- xrlelttrt ***************)

lemma MMI_mtbird: assumes Amin: "φ ⟶ ¬ ( ch )" and
    Amaj: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ¬ ( ψ )"
   using assms by auto

lemma MMI_pm2_21d: assumes A1: "φ ⟶ ¬ ( ψ )"   
   shows "φ ⟶ ( ψ ⟶ ch )"
   using assms by auto

lemma MMI_3jaodan: assumes A1: "( φ ∧ ψ ) ⟶ ch" and
    A2: "( φ ∧ θ ) ⟶ ch" and
    A3: "( φ ∧ τ ) ⟶ ch"   
   shows "( φ ∧ ( ψ ∨ θ ∨ τ ) ) ⟶ ch"
   using assms by auto

lemma MMI_sylan2br: assumes A1: "( φ ∧ ψ ) ⟶ ch" and
    A2: "ψ ⟷ θ"   
   shows "( φ ∧ θ ) ⟶ ch"
   using assms by auto

lemma MMI_3jaoian: assumes A1: "( φ ∧ ψ ) ⟶ ch" and
    A2: "( θ ∧ ψ ) ⟶ ch" and
    A3: "( τ ∧ ψ ) ⟶ ch"   
   shows "( ( φ ∨ θ ∨ τ ) ∧ ψ ) ⟶ ch"
   using assms by auto

lemma MMI_mtbid: assumes Amin: "φ ⟶ ¬ ( ψ )" and
    Amaj: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ¬ ( ch )"
   using assms by auto

lemma MMI_con1d: assumes A1: "φ ⟶ ( ¬ ( ψ ) ⟶ ch )"   
   shows "φ ⟶ ( ¬ ( ch ) ⟶ ψ )"
   using assms by auto

lemma MMI_pm2_21nd: assumes A1: "φ ⟶ ψ"   
   shows "φ ⟶ ( ¬ ( ψ ) ⟶ ch )"
   using assms by auto

lemma MMI_syl3an1b: assumes A1: "( φ ∧ ψ ∧ ch ) ⟶ θ" and
    A2: "τ ⟷ φ"   
   shows "( τ ∧ ψ ∧ ch ) ⟶ θ"
   using assms by auto

lemma MMI_adantld: assumes A1: "φ ⟶ ( ψ ⟶ ch )"   
   shows "φ ⟶ ( ( θ ∧ ψ ) ⟶ ch )"
   using assms by auto

lemma MMI_adantrd: assumes A1: "φ ⟶ ( ψ ⟶ ch )"   
   shows "φ ⟶ ( ( ψ ∧ θ ) ⟶ ch )"
   using assms by auto

lemma MMI_anasss: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) ⟶ θ"   
   shows "( φ ∧ ( ψ ∧ ch ) ) ⟶ θ"
   using assms by auto

lemma MMI_syl3an3b: assumes A1: "( φ ∧ ψ ∧ ch ) ⟶ θ" and
    A2: "τ ⟷ ch"   
   shows "( φ ∧ ψ ∧ τ ) ⟶ θ"
   using assms by auto

(**************xrltletrt-lttri3***********************)


lemma MMI_mpbid: assumes Amin: "φ ⟶ ψ" and
    Amaj: "φ ⟶ ( ψ ⟷ ch )"   
   shows "φ ⟶ ch"
   using assms by auto

lemma MMI_orbi12d: assumes A1: "φ ⟶ ( ψ ⟷ ch )" and
    A2: "φ ⟶ ( θ ⟷ τ )"   
   shows "φ ⟶ ( ( ψ ∨ θ ) ⟷ ( ch ∨ τ ) )"
   using assms by auto

lemma MMI_ianor: 
   shows "¬ ( φ ∧ ψ ) ⟷ ¬ φ ∨ ¬ ψ "
  by auto

lemma MMI_bitr2: assumes A1: "φ ⟷ ψ" and
    A2: "ψ ⟷ ch"   
   shows "ch ⟷ φ"
   using assms by auto

lemma MMI_biimp: assumes A1: "φ ⟷ ψ"   
   shows "φ ⟶ ψ"
   using assms by auto

lemma MMI_mpan2d: assumes A1: "φ ⟶ ch" and
    A2: "φ ⟶ ( ( ψ ∧ ch ) ⟶ θ )"   
   shows "φ ⟶ ( ψ ⟶ θ )"
   using assms by auto

lemma MMI_ad2antrr: assumes A1: "φ ⟶ ψ"   
   shows "( ( φ ∧ ch ) ∧ θ ) ⟶ ψ"
   using assms by auto

lemma MMI_biimpac: assumes A1: "φ ⟶ ( ψ ⟷ ch )"   
   shows "( ψ ∧ φ ) ⟶ ch"
   using assms by auto

(***********letri3-ltne**************************)

lemma MMI_con2bii: assumes A1: "φ ⟷ ¬ ( ψ )"   
   shows "ψ ⟷ ¬ ( φ )"
   using assms by auto

lemma MMI_pm3_26bd: assumes A1: "φ ⟷ ( ψ ∧ ch )"   
   shows "φ ⟶ ψ"
   using assms by auto

(******* le2tri3 - leadd2 ***********************)

lemma MMI_biimpr: assumes A1: "φ ⟷ ψ"   
   shows "ψ ⟶ φ"
   using assms by auto

lemma (in MMIsar0) MMI_3brtr3g: assumes A1: "φ ⟶ A \<ls> B" and
    A2: "A = C" and
    A3: "B = D"   
   shows "φ ⟶ C \<ls> D"
   using assms by auto

lemma (in MMIsar0) MMI_breq12i: assumes A1: "A = B" and
    A2: "C = D"   
   shows 
  "A \<ls> C ⟷ B \<ls> D"
  "A \<lsq> C ⟷ B \<lsq> D"
   using assms by auto

lemma MMI_negbii: assumes Aa: "φ ⟷ ψ"   
   shows "¬φ ⟷ ¬ψ"
   using assms by auto

(********* ltsubadd - addgt0 ***************)

lemma (in MMIsar0) MMI_breq1i: assumes A1: "A = B"   
   shows 
  "A \<ls> C ⟷ B \<ls> C"
  "A \<lsq> C ⟷ B \<lsq> C"
   using assms by auto

(****** addge0 - ltneg **********************)

lemma MMI_syl5eqr: assumes A1: "φ ⟶ A = B" and
    A2: "A = C"   
   shows "φ ⟶ C = B"
   using assms by auto

lemma (in MMIsar0) MMI_breq2d: assumes A1: "φ ⟶ A = B"   
   shows 
   "φ ⟶ C \<ls> A ⟷ C \<ls> B"
   "φ ⟶ C \<lsq> A ⟷ C \<lsq> B"
   using assms by auto

lemma MMI_ccase: assumes A1: "φ ∧ ψ ⟶ τ" and
    A2: "ch ∧ ψ ⟶ τ" and
    A3: "φ ∧ θ ⟶ τ" and
    A4: "ch ∧ θ ⟶ τ"   
   shows "(φ ∨ ch) ∧ (ψ ∨ θ) ⟶ τ"
   using assms by auto

lemma MMI_pm3_27bd: assumes A1: "φ ⟷ ψ ∧ ch"   
   shows "φ ⟶ ch"
   using assms by auto

lemma MMI_nsyl3: assumes A1: "φ ⟶ ¬ψ" and
    A2: "ch ⟶ ψ"   
   shows "ch ⟶ ¬φ"
   using assms by auto

lemma MMI_jctild: assumes A1: "φ ⟶ ψ ⟶ ch" and
    A2: "φ ⟶ θ"   
   shows "φ ⟶ 
   ψ ⟶ θ ∧ ch"
   using assms by auto

lemma MMI_jctird: assumes A1: "φ ⟶ ψ ⟶ ch" and
    A2: "φ ⟶ θ"   
   shows "φ ⟶ 
   ψ ⟶ ch ∧ θ"
   using assms by auto

lemma MMI_ccase2: assumes A1: "φ ∧ ψ ⟶ τ" and
    A2: "ch ⟶ τ" and
    A3: "θ ⟶ τ"   
   shows "(φ ∨ ch) ∧ (ψ ∨ θ) ⟶ τ"
   using assms by auto

(******** leneg - msqgt0 **************)

lemma MMI_3bitr3r: assumes A1: "φ ⟷ ψ" and
    A2: "φ ⟷ ch" and
    A3: "ψ ⟷ θ"   
   shows "θ ⟷ ch"
   using assms by auto

lemma (in MMIsar0) MMI_syl6breq: assumes A1: "φ ⟶ A \<ls> B" and
    A2: "B = C"   
   shows 
  "φ ⟶ A \<ls>  C"
   using assms by auto

(********* msqge0 - addge01t ******************)

lemma MMI_pm2_61i: assumes A1: "φ ⟶ ψ" and
    A2: "¬φ ⟶ ψ"   
   shows "ψ"
   using assms by auto

lemma MMI_syl6req: assumes A1: "φ ⟶ A = B" and
    A2: "B = C"   
   shows "φ ⟶ C = A"
   using assms by auto

lemma MMI_pm2_61d: assumes A1: "φ ⟶ ψ ⟶ ch" and
    A2: "φ ⟶ 
   ¬ψ ⟶ ch"   
   shows "φ ⟶ ch"
   using assms by auto

lemma MMI_orim1d: assumes A1: "φ ⟶ ψ ⟶ ch"   
   shows "φ ⟶ 
   ψ ∨ θ ⟶ ch ∨ θ"
   using assms by auto

lemma (in MMIsar0) MMI_breq1d: assumes A1: "φ ⟶ A = B"   
   shows 
  "φ ⟶ A \<ls> C ⟷ B \<ls> C"
  "φ ⟶ A \<lsq> C ⟷ B \<lsq> C"
   using assms by auto

lemma (in MMIsar0) MMI_breq12d: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ C = D"   
   shows 
  "φ ⟶ A \<ls> C ⟷ B \<ls> D"
  "φ ⟶ A \<lsq> C ⟷ B \<lsq> D"
   using assms by auto

lemma MMI_bibi2d: assumes A1: "φ ⟶ 
   ψ ⟷ ch"   
   shows "φ ⟶ 
   (θ ⟷ ψ) ⟷ 
   θ ⟷ ch"
   using assms by auto

(********* addge02t - leaddsubt *************)

lemma MMI_con4bid: assumes A1: "φ ⟶ 
   ¬ψ ⟷ ¬ch"   
   shows "φ ⟶ 
   ψ ⟷ ch"
   using assms by auto

lemma MMI_3com13: assumes A1: "φ ∧ ψ ∧ ch ⟶ θ"   
   shows "ch ∧ ψ ∧ φ ⟶ θ"
   using assms by auto

lemma MMI_3bitr3rd: assumes A1: "φ ⟶ 
   ψ ⟷ ch" and
    A2: "φ ⟶ 
   ψ ⟷ θ" and
    A3: "φ ⟶ 
   ch ⟷ τ"   
   shows "φ ⟶ 
   τ ⟷ θ"
   using assms by auto

(*********** leaddsub2t - lt2addt ***************)
lemma MMI_3imtr4g: assumes A1: "φ ⟶ ψ ⟶ ch" and
    A2: "θ ⟷ ψ" and
    A3: "τ ⟷ ch"   
   shows "φ ⟶ 
   θ ⟶ τ"
   using assms by auto

lemma MMI_expcom: assumes A1: "φ ∧ ψ ⟶ ch"   
   shows "ψ ⟶ φ ⟶ ch"
   using assms by auto

lemma (in MMIsar0) MMI_breq2i: assumes A1: "A = B"   
   shows 
  "C \<ls> A ⟷ C \<ls> B"
  "C \<lsq> A ⟷ C \<lsq> B"
   using assms by auto

lemma MMI_3bitr2r: assumes A1: "φ ⟷ ψ" and
    A2: "ch ⟷ ψ" and
    A3: "ch ⟷ θ"   
   shows "θ ⟷ φ"
   using assms by auto

lemma MMI_dedth4h: assumes A1: "A =  if(φ, A, R) ⟶ 
   τ ⟷ η" and
    A2: "B =  if(ψ, B, S) ⟶ 
   η ⟷ ζ" and
    A3: "C =  if(ch, C, F) ⟶ 
   ζ ⟷ si" and
    A4: "D =  if(θ, D, G) ⟶ si ⟷ rh" and
    A5: "rh"   
   shows "(φ ∧ ψ) ∧ ch ∧ θ ⟶ τ"
   using assms by auto

lemma MMI_anbi1d: assumes A1: "φ ⟶ 
   ψ ⟷ ch"   
   shows "φ ⟶ 
   ψ ∧ θ ⟷ ch ∧ θ"
   using assms by auto


(******** le2addt - posdift *********************)

lemma (in MMIsar0) MMI_breqtrrd: assumes A1: "φ ⟶ A \<ls> B" and
    A2: "φ ⟶ C = B"   
   shows "φ ⟶ A \<ls> C"
   using assms by auto

(******* ltnegt - posdif *****************)

lemma MMI_syl3an: assumes A1: "φ ∧ ψ ∧ ch ⟶ θ" and
    A2: "τ ⟶ φ" and
    A3: "η ⟶ ψ" and
    A4: "ζ ⟶ ch"   
   shows "τ ∧ η ∧ ζ ⟶ θ"
   using assms by auto

lemma MMI_3bitrd: assumes A1: "φ ⟶ 
   ψ ⟷ ch" and
    A2: "φ ⟶ 
   ch ⟷ θ" and
    A3: "φ ⟶ 
   θ ⟷ τ"   
   shows "φ ⟶ 
   ψ ⟷ τ"
   using assms by auto

(************ ltnegcon1 - lt01 **********************)

lemma (in MMIsar0) MMI_breqtr: assumes A1: "A \<ls> B" and
    A2: "B = C"   
   shows "A \<ls> C"
   using assms by auto

(*********** eqneg - ltp1 ********************)

lemma MMI_mpi: assumes A1: "ψ" and
    A2: "φ ⟶ ψ ⟶ ch"   
   shows "φ ⟶ ch"
   using assms by auto

lemma MMI_eqtr2: assumes A1: "A = B" and
    A2: "B = C"   
   shows "C = A"
   using assms by auto

lemma MMI_eqneqi: assumes A1: "A = B ⟷ C = D"   
   shows "A ≠ B ⟷ C ≠ D"
   using assms by auto

lemma (in MMIsar0) MMI_eqbrtrrd: assumes A1: "φ ⟶ A = B" and
    A2: "φ ⟶ A \<ls> C"   
   shows "φ ⟶ B \<ls> C"
   using assms by auto

lemma MMI_mpd: assumes A1: "φ ⟶ ψ" and
    A2: "φ ⟶ ψ ⟶ ch"   
   shows "φ ⟶ ch"
   using assms by auto

lemma MMI_mpdan: assumes A1: "φ ⟶ ψ" and
    A2: "φ ∧ ψ ⟶ ch"   
   shows "φ ⟶ ch"
   using assms by auto

(************ recgt0i - ltdiv1i ***************)

lemma (in MMIsar0) MMI_breqtrd: assumes A1: "φ ⟶ A \<ls> B" and
    A2: "φ ⟶ B = C"   
   shows "φ ⟶ A \<ls> C"
   using assms by auto

lemma MMI_mpand: assumes A1: "φ ⟶ ψ" and
    A2: "φ ⟶ 
   ψ ∧ ch ⟶ θ"   
   shows "φ ⟶ ch ⟶ θ"
   using assms by auto

lemma MMI_imbi1d: assumes A1: "φ ⟶ 
   ψ ⟷ ch"   
   shows "φ ⟶ 
   (ψ ⟶ θ) ⟷ 
   (ch ⟶ θ)"
   using assms by auto

lemma MMI_mtbii: assumes Amin: "¬ψ" and
    Amaj: "φ ⟶ 
   ψ ⟷ ch"   
   shows "φ ⟶ ¬ch"
   using assms by auto

(********** ltdiv1 - lemul2t **************)

lemma MMI_sylan2d: assumes A1: "φ ⟶ 
   ψ ∧ ch ⟶ θ" and
    A2: "φ ⟶ τ ⟶ ch"   
   shows "φ ⟶ 
   ψ ∧ τ ⟶ θ"
   using assms by auto

(********* ltmul2 - ltmulgt12t ***********)
lemma MMI_imp32: assumes A1: "φ ⟶ 
   ψ ⟶ ch ⟶ θ"   
   shows "φ ∧ ψ ∧ ch ⟶ θ"
   using assms by auto

lemma (in MMIsar0) MMI_breqan12d: assumes A1: "φ ⟶ A = B" and
    A2: "ψ ⟶ C = D"   
   shows 
  "φ ∧ ψ ⟶  A \<ls> C ⟷ B \<ls> D"
  "φ ∧ ψ ⟶  A \<lsq> C ⟷ B \<lsq> D"
   using assms by auto

lemma MMI_a1dd: assumes A1: "φ ⟶ ψ ⟶ ch"   
   shows "φ ⟶ 
   ψ ⟶ θ ⟶ ch"
   using assms by auto

lemma (in MMIsar0) MMI_3brtr3d: assumes A1: "φ ⟶ A \<lsq> B" and
    A2: "φ ⟶ A = C" and
    A3: "φ ⟶ B = D"   
   shows "φ ⟶ C \<lsq> D"
   using assms by auto

lemma MMI_ad2antll: assumes A1: "φ ⟶ ψ"   
   shows "ch ∧ θ ∧ φ ⟶ ψ"
   using assms by auto

lemma MMI_adantrrl: assumes A1: "φ ∧ ψ ∧ ch ⟶ θ"   
   shows "φ ∧ ψ ∧ τ ∧ ch ⟶ θ"
   using assms by auto

lemma MMI_syl2ani: assumes A1: "φ ⟶ 
   ψ ∧ ch ⟶ θ" and
    A2: "τ ⟶ ψ" and
    A3: "η ⟶ ch"   
   shows "φ ⟶ 
   τ ∧ η ⟶ θ"
   using assms by auto

lemma MMI_im2anan9: assumes A1: "φ ⟶ ψ ⟶ ch" and
    A2: "θ ⟶ 
   τ ⟶ η"   
   shows "φ ∧ θ ⟶ 
   ψ ∧ τ ⟶ ch ∧ η"
   using assms by auto

lemma MMI_ancomsd: assumes A1: "φ ⟶ 
   ψ ∧ ch ⟶ θ"   
   shows "φ ⟶ 
   ch ∧ ψ ⟶ θ"
   using assms by auto

lemma MMI_mpani: assumes A1: "ψ" and
    A2: "φ ⟶ 
   ψ ∧ ch ⟶ θ"   
   shows "φ ⟶ ch ⟶ θ"
   using assms by auto

lemma MMI_syldan: assumes A1: "φ ∧ ψ ⟶ ch" and
    A2: "φ ∧ ch ⟶ θ"   
   shows "φ ∧ ψ ⟶ θ"
   using assms by auto

lemma MMI_mp3anl1: assumes A1: "φ" and
    A2: "(φ ∧ ψ ∧ ch) ∧ θ ⟶ τ"   
   shows "(ψ ∧ ch) ∧ θ ⟶ τ"
   using assms by auto

lemma MMI_3ad2ant1: assumes A1: "φ ⟶ ch"   
   shows "φ ∧ ψ ∧ θ ⟶ ch"
   using assms by auto

(********* lemulge11t - divgt0i2 ***********)

lemma MMI_pm3_2: 
   shows "φ ⟶ 
   ψ ⟶ φ ∧ ψ"
  by auto

lemma MMI_pm2_43i: assumes A1: "φ ⟶ 
   φ ⟶ ψ"   
   shows "φ ⟶ ψ"
   using assms by auto

lemma MMI_jctil: assumes A1: "φ ⟶ ψ" and
    A2: "ch"   
   shows "φ ⟶ ch ∧ ψ"
   using assms by auto

lemma MMI_mpanl12: assumes A1: "φ" and
    A2: "ψ" and
    A3: "(φ ∧ ψ) ∧ ch ⟶ θ"   
   shows "ch ⟶ θ"
   using assms by auto

(********* divgt0i - ledivmul2t ***************)

lemma MMI_mpanr1: assumes A1: "ψ" and
    A2: "φ ∧ ψ ∧ ch ⟶ θ"   
   shows "φ ∧ ch ⟶ θ"
   using assms by auto

lemma MMI_ad2antrl: assumes A1: "φ ⟶ ψ"   
   shows "ch ∧ φ ∧ θ ⟶ ψ"
   using assms by auto

lemma MMI_3adant3r: assumes A1: "φ ∧ ψ ∧ ch ⟶ θ"   
   shows "φ ∧ ψ ∧ ch ∧ τ ⟶ θ"
   using assms by auto

lemma MMI_3adant1l: assumes A1: "φ ∧ ψ ∧ ch ⟶ θ"   
   shows "(τ ∧ φ) ∧ ψ ∧ ch ⟶ θ"
   using assms by auto

lemma MMI_3adant2r: assumes A1: "φ ∧ ψ ∧ ch ⟶ θ"   
   shows "φ ∧ (ψ ∧ τ) ∧ ch ⟶ θ"
   using assms by auto

(********** lemuldivt - lerect ****************)

lemma MMI_3bitr4rd: assumes A1: "φ ⟶ 
   ψ ⟷ ch" and
    A2: "φ ⟶ 
   θ ⟷ ψ" and
    A3: "φ ⟶ 
   τ ⟷ ch"   
   shows "φ ⟶ 
   τ ⟷ θ"
   using assms by auto

lemma MMI_3anrev: 
   shows "φ ∧ ψ ∧ ch ⟷ ch ∧ ψ ∧ φ"
  by auto

lemma MMI_eqtr4: assumes A1: "A = B" and
    A2: "C = B"   
   shows "A = C"
   using assms by auto

lemma MMI_anidm: 
   shows "φ ∧ φ ⟷ φ"
  by auto

lemma MMI_bi2anan9r: assumes A1: "φ ⟶ 
   ψ ⟷ ch" and
    A2: "θ ⟶ 
   τ ⟷ η"   
   shows "θ ∧ φ ⟶ 
   ψ ∧ τ ⟷ ch ∧ η"
   using assms by auto

lemma MMI_3imtr3g: assumes A1: "φ ⟶ ψ ⟶ ch" and
    A2: "ψ ⟷ θ" and
    A3: "ch ⟷ τ"   
   shows "φ ⟶ 
   θ ⟶ τ"
   using assms by auto

lemma MMI_a3d: assumes A1: "φ ⟶ 
   ¬ψ ⟶ ¬ch"   
   shows "φ ⟶ ch ⟶ ψ"
   using assms by auto

lemma MMI_sylan9bbr: assumes A1: "φ ⟶ 
   ψ ⟷ ch" and
    A2: "θ ⟶ 
   ch ⟷ τ"   
   shows "θ ∧ φ ⟶ 
   ψ ⟷ τ"
   using assms by auto

lemma MMI_sylan9bb: assumes A1: "φ ⟶ 
   ψ ⟷ ch" and
    A2: "θ ⟶ 
   ch ⟷ τ"   
   shows "φ ∧ θ ⟶ 
   ψ ⟷ τ"
   using assms by auto

lemma MMI_3bitr3g: assumes A1: "φ ⟶ 
   ψ ⟷ ch" and
    A2: "ψ ⟷ θ" and
    A3: "ch ⟷ τ"   
   shows "φ ⟶ 
   θ ⟷ τ"
   using assms by auto

lemma MMI_pm5_21: 
   shows "¬φ ∧ ¬ψ ⟶ 
   φ ⟷ ψ"
  by auto

(******** lerectOLD - ltdiv23 ************)

lemma MMI_an6: 
   shows "(φ ∧ ψ ∧ ch) ∧ θ ∧ τ ∧ η ⟷ 
   (φ ∧ θ) ∧ (ψ ∧ τ) ∧ ch ∧ η"
  by auto

lemma MMI_syl3anl1: assumes A1: "(φ ∧ ψ ∧ ch) ∧ θ ⟶ τ" and
    A2: "η ⟶ φ"   
   shows "(η ∧ ψ ∧ ch) ∧ θ ⟶ τ"
   using assms by auto

lemma MMI_imp4a: assumes A1: "φ ⟶ 
   ψ ⟶ 
   ch ⟶ 
   θ ⟶ τ"   
   shows "φ ⟶ 
   ψ ⟶ 
   ch ∧ θ ⟶ τ"
   using assms by auto

lemma (in MMIsar0) MMI_breqan12rd: assumes A1: "φ ⟶ A = B" and
    A2: "ψ ⟶ C = D"   
   shows 
  "ψ ∧ φ ⟶  A \<ls> C ⟷ B \<ls> D"
  "ψ ∧ φ ⟶  A \<lsq> C ⟷ B \<lsq> D"
   using assms by auto

(****** lediv23t - halfpos ******************)

lemma (in MMIsar0) MMI_3brtr4d: assumes A1: "φ ⟶ A \<ls> B" and
    A2: "φ ⟶ C = A" and
    A3: "φ ⟶ D = B"   
   shows "φ ⟶ C \<ls> D"
   using assms by auto

lemma MMI_adantrrr: assumes A1: "φ ∧ ψ ∧ ch ⟶ θ"   
   shows "φ ∧ ψ ∧ ch ∧ τ ⟶ θ"
   using assms by auto

lemma MMI_adantrlr: assumes A1: "φ ∧ ψ ∧ ch ⟶ θ"   
   shows "φ ∧ (ψ ∧ τ) ∧ ch ⟶ θ"
   using assms by auto

lemma MMI_imdistani: assumes A1: "φ ⟶ ψ ⟶ ch"   
   shows "φ ∧ ψ ⟶ φ ∧ ch"
   using assms by auto

lemma MMI_anabss3: assumes A1: "(φ ∧ ψ) ∧ ψ ⟶ ch"   
   shows "φ ∧ ψ ⟶ ch"
   using assms by auto

lemma MMI_mp3anl2: assumes A1: "ψ" and
    A2: "(φ ∧ ψ ∧ ch) ∧ θ ⟶ τ"   
   shows "(φ ∧ ch) ∧ θ ⟶ τ"
   using assms by auto

(****** ledivp1t - squeeze0 ****************)

lemma MMI_mpanl2: assumes A1: "ψ" and
    A2: "(φ ∧ ψ) ∧ ch ⟶ θ"   
   shows "φ ∧ ch ⟶ θ"
   using assms by auto

lemma MMI_mpancom: assumes A1: "ψ ⟶ φ" and
    A2: "φ ∧ ψ ⟶ ch"   
   shows "ψ ⟶ ch"
   using assms by auto

lemma MMI_or12: 
   shows "φ ∨ ψ ∨ ch ⟷ ψ ∨ φ ∨ ch"
  by auto

lemma MMI_rcla4ev: assumes A1: "∀x. x = A ⟶  φ(x) ⟷ ψ"   
   shows "A ∈ B ∧ ψ ⟶ ( ∃x∈B. φ(x) )"
   using assms by auto

lemma MMI_jctir: assumes A1: "φ ⟶ ψ" and
    A2: "ch"   
   shows "φ ⟶ ψ ∧ ch"
   using assms by auto

lemma MMI_iffalse: 
   shows "¬φ ⟶  if(φ, A, B) = B"
  by auto

lemma MMI_iftrue: 
   shows "φ ⟶  if(φ, A, B) = A"
  by auto

lemma MMI_pm2_61d2: assumes A1: "φ ⟶ 
   ¬ψ ⟶ ch" and
    A2: "ψ ⟶ ch"   
   shows "φ ⟶ ch"
   using assms by auto

lemma MMI_pm2_61dan: assumes A1: "φ ∧ ψ ⟶ ch" and
    A2: "φ ∧ ¬ψ ⟶ ch"   
   shows "φ ⟶ ch"
   using assms by auto

lemma MMI_orcanai: assumes A1: "φ ⟶ ψ ∨ ch"   
   shows "φ ∧ ¬ψ ⟶ ch"
   using assms by auto

lemma MMI_ifcl: 
   shows "A ∈ C ∧ B ∈ C ⟶  if(φ, A, B) ∈ C"
  by auto

lemma MMI_imim2i: assumes A1: "φ ⟶ ψ"   
   shows "(ch ⟶ φ) ⟶ ch ⟶ ψ"
   using assms by auto

lemma MMI_com13: assumes A1: "φ ⟶ 
   ψ ⟶ ch ⟶ θ"   
   shows "ch ⟶ 
   ψ ⟶ 
   φ ⟶ θ"
   using assms by auto

lemma MMI_rcla4v: assumes A1: "∀x. x = A ⟶  φ(x) ⟷ ψ"   
   shows "A ∈ B ⟶  (∀x∈B. φ(x)) ⟶ ψ"
   using assms by auto

lemma MMI_syl5d: assumes A1: "φ ⟶ 
   ψ ⟶ ch ⟶ θ" and
    A2: "φ ⟶ τ ⟶ ch"   
   shows "φ ⟶ 
   ψ ⟶ 
   τ ⟶ θ"
   using assms by auto

lemma MMI_eqcoms: assumes A1: "A = B ⟶ φ"   
   shows "B = A ⟶ φ"
   using assms by auto

(******* nnssre - nnex **************)

lemma MMI_rgen: assumes A1: "∀x. x ∈ A ⟶ φ(x)"   
   shows "∀x∈A. φ(x)"
   using assms by auto

lemma (in MMIsar0) MMI_reex: 
   shows "ℝ = ℝ"
  by auto

lemma MMI_sstri: assumes A1: "A ⊆B" and
    A2: "B ⊆C"   
   shows "A ⊆C"
   using assms by auto

lemma MMI_ssexi: assumes A1: "B = B" and
    A2: "A ⊆B"   
   shows "A = A"
   using assms by auto


end