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.

*)

header {*\isaheader{MMI\_logic\_and\_sets.thy}*} 

theory MMI_logic_and_sets imports MMI_prelude

begin

section{*Basic Metamath theorems*}

text{* This section contains Metamath theorems that the more advanced 
  theorems from @{text "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. *}   

lemma MMI_ax_mp: assumes "φ" and "φ --> ψ" shows "ψ"
  using prems by auto;

lemma MMI_sseli: assumes A1: "A ⊆ B"   
   shows "C ∈ A --> C ∈ B"
   using prems by auto

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

lemma MMI_syl: assumes A1: "φ --> ps" and
    A2: "ps --> ch"   
   shows "φ --> ch"
   using prems 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 prems by auto;

lemma MMI_xpex: assumes A1: "A isASet" and
    A2: "B isASet"   
   shows "( A × B ) isASet"
   using prems 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 prems by auto

lemma MMI_3coml: assumes A1: "( φ ∧ ψ ∧ chi ) --> th"   
   shows "( ψ ∧ chi ∧ φ ) --> th"
   using prems by auto;

lemma MMI_sylan: assumes A1: "( φ ∧ ψ ) --> chi" and
    A2: "th --> φ"   
   shows "( th ∧ ψ ) --> chi"
   using prems by auto;

lemma MMI_3impa: assumes A1: "( ( φ ∧ ψ ) ∧ chi ) --> th"   
   shows "( φ ∧ ψ ∧ chi ) --> th"
   using prems by auto;

lemma MMI_3adant2: assumes A1: "( φ ∧ ψ ) --> chi"   
   shows "( φ ∧ th ∧ ψ ) --> chi"
   using prems by auto;

lemma MMI_3adant1: assumes A1: "( φ ∧ ψ ) --> chi"   
   shows "( th ∧ φ ∧ ψ ) --> chi"
   using prems 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 prems by auto;

lemma MMI_mp2an: assumes A1: "φ" and
    A2: "ψ" and
    A3: "( φ ∧ ψ ) --> chi"   
   shows "chi"
   using prems by auto;

lemma MMI_mp3an: assumes A1: "φ" and
    A2: "ψ" and
    A3: "ch" and
    A4: "( φ ∧ ψ ∧ ch ) --> ϑ"   
   shows "ϑ"
   using prems by auto

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

lemma MMI_eqtr: assumes A1: "A = B" and
    A2: "B = C"   
   shows "A = C"
   using prems 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 prems by auto;

lemma MMI_eqeq12d: assumes A1: "φ --> A = B" and
    A2: "φ --> C = D"   
   shows "φ --> ( A = C <-> B = D )"
   using prems by auto

lemma MMI_mpan2: assumes A1: "ψ" and
    A2: "( φ ∧ ψ ) --> ch"   
   shows "φ --> ch"
   using prems 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 prems by auto

lemma MMI_adantr: assumes A1: "φ --> ψ"   
   shows "( φ ∧ ch ) --> ψ"
   using prems by auto

lemma MMI_mpan: assumes A1: "φ" and
    A2: "( φ ∧ ψ ) --> ch"   
   shows "ψ --> ch"
   using prems by auto;

lemma MMI_eqeq1d: assumes A1: "φ --> A = B"   
   shows "φ --> ( A = C <-> B = C )"
   using prems 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 prems by auto

lemma MMI_syl6bi: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "ch --> ϑ"   
   shows "φ --> ( ψ --> ϑ )"
   using prems by auto

lemma MMI_imp: assumes A1: "φ --> ( ψ --> ch )"   
   shows "( φ ∧ ψ ) --> ch"
   using prems by auto

lemma MMI_sylibd: assumes A1: "φ --> ( ψ --> ch )" and
    A2: "φ --> ( ch <-> ϑ )"   
   shows "φ --> ( ψ --> ϑ )"
   using prems by auto

lemma MMI_ex: assumes A1: "( φ ∧ ψ ) --> ch"   
   shows "φ --> ( ψ --> ch )"
   using prems by auto

lemma MMI_r19_23aiv: assumes A1: "∀x.  (x ∈ A  --> (φ(x) --> ψ ))"   
   shows "( ∃ x ∈ A . φ(x) ) --> ψ"
  using prems by auto;

lemma MMI_bitr: assumes A1: "φ <-> ψ" and
    A2: "ψ <-> ch"   
   shows "φ <-> ch"
   using prems by auto

lemma MMI_eqeq12i: assumes A1: "A = B" and
    A2: "C = D"   
   shows "A = C <-> B = D"
   using prems 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 prems by auto

lemma MMI_bibi1d: assumes A1: "φ --> ( ψ <-> ch )"   
   shows "φ --> ( ( ψ <-> ϑ ) <-> ( ch <-> ϑ ) )"
   using prems 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 prems by auto

lemma MMI_eqeq2d: assumes A1: "φ --> A = B"   
   shows "φ --> ( C = A <-> C = B )"
   using prems 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 prems by auto

lemma MMI_3adant3: assumes A1: "( φ ∧ ψ ) --> ch"   
   shows "( φ ∧ ψ ∧ ϑ ) --> ch"
   using prems by auto

lemma MMI_bitr3d: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "φ --> ( ψ <-> ϑ )"   
   shows "φ --> ( ch <-> ϑ )"
   using prems 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 prems 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 prems by auto;

lemma MMI_3com12: assumes A1: "( φ ∧ ψ ∧ ch ) --> ϑ"   
   shows "( ψ ∧ φ ∧ ch ) --> ϑ"
   using prems 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 prems by auto;

lemma MMI_3com23: assumes A1: "( φ ∧ ψ ∧ ch ) --> ϑ"   
   shows "( φ ∧ ch ∧ ψ ) --> ϑ"
   using prems by auto;

lemma MMI_3expa: assumes A1: "( φ ∧ ψ ∧ ch ) --> ϑ"   
   shows "( ( φ ∧ ψ ) ∧ ch ) --> ϑ"
   using prems by auto;

lemma MMI_adantrr: assumes A1: "( φ ∧ ψ ) --> ch"   
   shows "( φ ∧ ( ψ ∧ ϑ ) ) --> ch"
   using prems by auto;

lemma MMI_3expb: assumes A1: "( φ ∧ ψ ∧ ch ) --> ϑ"   
   shows "( φ ∧ ( ψ ∧ ch ) ) --> ϑ"
   using prems by auto;

lemma MMI_an4s: assumes A1: "( ( φ ∧ ψ ) ∧ ( ch ∧ ϑ ) ) --> τ"   
   shows "( ( φ ∧ ch ) ∧ ( ψ ∧ ϑ ) ) --> τ"
   using prems by auto;

lemma MMI_eqtrd: assumes A1: "φ --> A = B" and
    A2: "φ --> B = C"   
   shows "φ --> A = C"
   using prems by auto;

lemma MMI_ad2ant2l: assumes A1: "( φ ∧ ψ ) --> ch"   
   shows "( ( ϑ ∧ φ ) ∧ ( τ ∧ ψ ) ) --> ch"
   using prems by auto;

lemma MMI_pm3_2i: assumes A1: "φ" and
    A2: "ψ"   
   shows "φ ∧ ψ"
   using prems 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 prems by auto;

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

lemma MMI_mpbir2an: assumes A1: "φ <-> ( ψ ∧ ch )" and
    A2: "ψ" and
    A3: "ch"   
   shows "φ"
   using prems 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 prems 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 prems by auto;

lemma MMI_mp3an13: assumes A1: "φ" and
    A2: "ch" and
    A3: "( φ ∧ ψ ∧ ch ) --> ϑ"   
   shows "ψ --> ϑ"
   using prems by auto;

lemma MMI_eqcomd: assumes A1: "φ --> A = B"   
   shows "φ --> B = A"
   using prems by auto;

lemma MMI_sylan9eqr: assumes A1: "φ --> A = B" and
    A2: "ψ --> B = C"   
   shows "( ψ ∧ φ ) --> A = C"
   using prems by auto;

lemma MMI_exp32: assumes A1: "( φ ∧ ( ψ ∧ ch ) ) --> ϑ"   
   shows "φ --> ( ψ --> ( ch --> ϑ ) )"
   using prems by auto;

lemma MMI_impcom: assumes A1: "φ --> ( ψ --> ch )"   
   shows "( ψ ∧ φ ) --> ch"
   using prems by auto;

lemma MMI_a1d: assumes A1: "φ --> ψ"   
   shows "φ --> ( ch --> ψ )"
   using prems by auto;

lemma MMI_r19_21aiv: assumes A1: "∀x. φ --> ( x ∈ A --> ψ(x) )"   
   shows "φ --> ( ∀ x ∈ A . ψ(x) )"
   using prems 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 prems by auto;

lemma MMI_mpid: assumes A1: "φ --> ch" and
    A2: "φ --> ( ψ --> ( ch --> ϑ ) )"   
   shows "φ --> ( ψ --> ϑ )"
   using prems 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 prems by auto;

lemma MMI_mp3an1: assumes A1: "φ" and
    A2: "( φ ∧ ψ ∧ ch ) --> ϑ"   
   shows "( ψ ∧ ch ) --> ϑ"
   using prems by auto;

lemma MMI_rgen2: assumes A1: "∀x y. ( x ∈ A ∧ y ∈ A ) --> φ(x,y)"   
   shows "∀ x ∈ A . ∀ y ∈ A . φ(x,y)"
   using prems 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 prems by auto;

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

lemma MMI_3imtr4: assumes A1: "φ --> ψ" and
    A2: "ch <-> φ" and
    A3: "ϑ <-> ψ"   
   shows "ch --> ϑ"
   using prems 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 prems 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 prems by auto

lemma MMI_albii: assumes A1: "φ <-> ψ"   
   shows "( ∀ x . φ ) <-> ( ∀ x . ψ )"
   using prems by auto;

(*************subcl-subadd **********************************)
lemma MMI_reucl: 
   shows "( ∃! x . x ∈ A ∧ φ(x) ) --> \<Union> { 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 " \<Union> { 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 prems by auto

lemma MMI_eleq1d: assumes A1: "φ --> A = B"   
   shows "φ --> ( A ∈ C <-> B ∈ C )"
   using prems by auto

lemma MMI_syl5eqel: assumes A1: "φ --> A ∈ B" and
    A2: "C = A"   
   shows "φ --> C ∈ B"
   using prems 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) <-> \<Union> { x ∈ A . φ(x) } = x"
proof;
  assume "φ(x)" 
  with A1 A2 show "\<Union> { x ∈ A . φ(x) } = x" by auto;
next assume A3: "\<Union> { 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) <-> \<Union> { x ∈ A . φ(x) } = x )"
  using IML_eeuni by simp;

lemma MMI_eqeq1i: assumes A1: "A = B"   
   shows "A = C <-> B = C"
   using prems by auto

lemma MMI_syl6rbbr: assumes A1: "∀x. φ(x) --> ( ψ(x) <-> ch(x) )" and
    A2: "∀x. ϑ(x) <-> ch(x)"   
   shows "∀ x. φ(x) --> ( ϑ(x) <-> ψ(x) )"
   using prems by auto;

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

lemma MMI_syl6rbbrA: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "ϑ <-> ch"   
   shows "φ --> ( ϑ <-> ψ )"
   using prems by auto;

lemma MMI_vtoclga: assumes A1: "∀x. x = A --> ( φ(x) <-> ψ)" and
    A2: "∀x. x ∈ B --> φ(x)"
   shows "A ∈ B --> ψ"
   using prems by auto;

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

lemma MMI_3bitr4: assumes A1: "φ <-> ψ" and
    A2: "ch <-> φ" and
    A3: "ϑ <-> ψ"   
   shows "ch <-> ϑ"
   using prems by auto

lemma MMI_mpbii: assumes Amin: "ψ" and
    Amaj: "φ --> ( ψ <-> ch )"   
   shows "φ --> ch"
   using prems 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 prems by auto

lemma MMI_syl3anc: assumes A1: "( φ ∧ ψ ∧ ch ) --> ϑ" and
    A2: "τ --> φ" and
    A3: "τ --> ψ" and
    A4: "τ --> ch"   
   shows "τ --> ϑ"
   using prems by auto

lemma MMI_syl5eq: assumes A1: "φ --> A = B" and
    A2: "C = A"   
   shows "φ --> C = B"
   using prems by auto

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

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

lemma MMI_mpbir: assumes Amin: "ψ" and
    Amaj: "φ <-> ψ"   
   shows "φ"
   using prems by auto

lemma MMI_syl3an3: assumes A1: "( φ ∧ ψ ∧ ch ) --> ϑ" and
    A2: "τ --> ch"   
   shows "( φ ∧ ψ ∧ τ ) --> ϑ"
   using prems by auto

lemma MMI_3eqtrd: assumes A1: "φ --> A = B" and
    A2: "φ --> B = C" and
    A3: "φ --> C = D"   
   shows "φ --> A = D"
   using prems by auto

lemma MMI_syl5: assumes A1: "φ --> ( ψ --> ch )" and
    A2: "ϑ --> ψ"   
   shows "φ --> ( ϑ --> ch )"
   using prems by auto

lemma MMI_exp3a: assumes A1: "φ --> ( ( ψ ∧ ch ) --> ϑ )"   
   shows "φ --> ( ψ --> ( ch --> ϑ ) )"
   using prems by auto

lemma MMI_com12: assumes A1: "φ --> ( ψ --> ch )"   
   shows "ψ --> ( φ --> ch )"
   using prems by auto

lemma MMI_3imp: assumes A1: "φ --> ( ψ --> ( ch --> ϑ ) )"   
   shows "( φ ∧ ψ ∧ ch ) --> ϑ"
   using prems by auto;

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

lemma MMI_3eqtr3: assumes A1: "A = B" and
    A2: "A = C" and
    A3: "B = D"   
   shows "C = D"
   using prems 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 prems by auto;

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

lemma MMI_dedth: assumes A1: "A = if ( φ , A , B ) --> ( ψ <-> ch )" and
    A2: "ch"   
   shows "φ --> ψ"
   using prems by auto

lemma MMI_id: 
   shows "φ --> φ"
  by auto

lemma MMI_eqtr3d: assumes A1: "φ --> A = B" and
    A2: "φ --> A = C"   
   shows "φ --> B = C"
   using prems by auto

lemma MMI_sylan2: assumes A1: "( φ ∧ ψ ) --> ch" and
    A2: "ϑ --> ψ"   
   shows "( φ ∧ ϑ ) --> ch"
   using prems by auto

lemma MMI_adantl: assumes A1: "φ --> ψ"   
   shows "( ch ∧ φ ) --> ψ"
   using prems 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 )"
  by auto

lemma MMI_anidms: assumes A1: "( φ ∧ φ ) --> ψ"   
   shows "φ --> ψ"
   using prems by auto;

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

lemma MMI_anabsan2: assumes A1: "( φ ∧ ( ψ ∧ ψ ) ) --> ch"   
   shows "( φ ∧ ψ ) --> ch"
   using prems 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 prems by auto

lemma MMI_3eqtr3g: assumes A1: "φ --> A = B" and
    A2: "A = C" and
    A3: "B = D"   
   shows "φ --> C = D"
   using prems by auto

lemma MMI_3bitr: assumes A1: "φ <-> ψ" and
    A2: "ψ <-> ch" and
    A3: "ch <-> ϑ"   
   shows "φ <-> ϑ"
   using prems by auto;

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

lemma MMI_3bitr3: assumes A1: "φ <-> ψ" and
    A2: "φ <-> ch" and
    A3: "ψ <-> ϑ"   
   shows "ch <-> ϑ"
   using prems by auto

lemma MMI_eqcom: 
   shows "A = B <-> B = A"
  by auto

lemma MMI_syl6bb: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "ch <-> ϑ"   
   shows "φ --> ( ψ <-> ϑ )"
   using prems by auto

lemma MMI_3bitr3d: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "φ --> ( ψ <-> ϑ )" and
    A3: "φ --> ( ch <-> τ )"   
   shows "φ --> ( ϑ <-> τ )"
   using prems by auto

lemma MMI_syl3an2: assumes A1: "( φ ∧ ψ ∧ ch ) --> ϑ" and
    A2: "τ --> ψ"   
   shows "( φ ∧ τ ∧ ch ) --> ϑ"
   using prems 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 prems by auto

lemma MMI_mp3an12: assumes A1: "φ" and
    A2: "ψ" and
    A3: "( φ ∧ ψ ∧ ch ) --> ϑ"   
   shows "ch --> ϑ"
   using prems by auto

lemma MMI_syl5bb: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "ϑ <-> ψ"   
   shows "φ --> ( ϑ <-> ch )"
   using prems 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 prems by auto

lemma MMI_19_23aiv: assumes A1: "∀x. φ(x) --> ψ"   
   shows "( ∃ x . φ(x) ) --> ψ"
   using prems by auto;

lemma MMI_eqeltrrd: assumes A1: "φ --> A = B" and
    A2: "φ --> A ∈ C"   
   shows "φ --> B ∈ C"
   using prems by auto

lemma MMI_syl2an: assumes A1: "( φ ∧ ψ ) --> ch" and
    A2: "ϑ --> φ" and
    A3: "τ --> ψ"   
   shows "( ϑ ∧ τ ) --> ch"
   using prems by auto;

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

lemma MMI_adantrl: assumes A1: "( φ ∧ ψ ) --> ch"   
   shows "( φ ∧ ( ϑ ∧ ψ ) ) --> ch"
   using prems by auto

lemma MMI_ad2ant2r: assumes A1: "( φ ∧ ψ ) --> ch"   
   shows "( ( φ ∧ ϑ ) ∧ ( ψ ∧ τ ) ) --> ch"
   using prems by auto

lemma MMI_adantll: assumes A1: "( φ ∧ ψ ) --> ch"   
   shows "( ( ϑ ∧ φ ) ∧ ψ ) --> ch"
   using prems by auto

lemma MMI_anandirs: assumes A1: "( ( φ ∧ ch ) ∧ ( ψ ∧ ch ) ) --> τ"   
   shows "( ( φ ∧ ψ ) ∧ ch ) --> τ"
   using prems by auto

lemma MMI_adantlr: assumes A1: "( φ ∧ ψ ) --> ch"   
   shows "( ( φ ∧ ϑ ) ∧ ψ ) --> ch"
   using prems by auto

lemma MMI_an42s: assumes A1: "( ( φ ∧ ψ ) ∧ ( ch ∧ ϑ ) ) --> τ"   
   shows "( ( φ ∧ ch ) ∧ ( ϑ ∧ ψ ) ) --> τ"
   using prems by auto;

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

lemma MMI_mp3an2: assumes A1: "ψ" and
    A2: "( φ ∧ ψ ∧ ch ) --> ϑ"   
   shows "( φ ∧ ch ) --> ϑ"
   using prems by auto;

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

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

lemma MMI_3impb: assumes A1: "( φ ∧ ( ψ ∧ ch ) ) --> ϑ"   
   shows "( φ ∧ ψ ∧ ch ) --> ϑ"
   using prems by auto

lemma MMI_mpbird: assumes Amin: "φ --> ch" and
    Amaj: "φ --> ( ψ <-> ch )"   
   shows "φ --> ψ"
   using prems 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 prems by auto

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

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

lemma MMI_eqtr4d: assumes A1: "φ --> A = B" and
    A2: "φ --> C = B"   
   shows "φ --> A = C"
   using prems by auto;

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

lemma MMI_3eqtr3rd: assumes A1: "φ --> A = B" and
    A2: "φ --> A = C" and
    A3: "φ --> B = D"   
   shows "φ --> D = C"
   using prems by auto

lemma MMI_sylanc: assumes A1: "( φ ∧ ψ ) --> ch" and
    A2: "ϑ --> φ" and
    A3: "ϑ --> ψ"   
   shows "ϑ --> ch"
   using prems by auto;

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

lemma MMI_anim12i: assumes A1: "φ --> ψ" and
    A2: "ch --> ϑ"   
   shows "( φ ∧ ch ) --> ( ψ ∧ ϑ )"
   using prems 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 prems by auto

lemma MMI_sylanr2: assumes A1: "( φ ∧ ( ψ ∧ ch ) ) --> ϑ" and
    A2: "τ --> ch"   
   shows "( φ ∧ ( ψ ∧ τ ) ) --> ϑ"
   using prems by auto

lemma MMI_sylanl2: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) --> ϑ" and
    A2: "τ --> ψ"   
   shows "( ( φ ∧ τ ) ∧ ch ) --> ϑ"
   using prems by auto

lemma MMI_ancom2s: assumes A1: "( φ ∧ ( ψ ∧ ch ) ) --> ϑ"   
   shows "( φ ∧ ( ch ∧ ψ ) ) --> ϑ"
   using prems by auto

lemma MMI_anandis: assumes A1: "( ( φ ∧ ψ ) ∧ ( φ ∧ ch ) ) --> τ"   
   shows "( φ ∧ ( ψ ∧ ch ) ) --> τ"
   using prems by auto

lemma MMI_sylan9eq: assumes A1: "φ --> A = B" and
    A2: "ψ --> B = C"   
   shows "( φ ∧ ψ ) --> A = C"
   using prems 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 prems by auto

lemma MMI_imbi12d: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "φ --> ( ϑ <-> τ )"   
   shows "φ --> ( ( ψ --> ϑ ) <-> ( ch --> τ ) )"
   using prems by auto

lemma MMI_bitrd: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "φ --> ( ch <-> ϑ )"   
   shows "φ --> ( ψ <-> ϑ )"
   using prems 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 prems by auto

lemma MMI_eqeq2i: assumes A1: "A = B"   
   shows "C = A <-> C = B"
   using prems by auto

lemma MMI_syl5bbr: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "ψ <-> ϑ"   
   shows "φ --> ( ϑ <-> ch )"
   using prems by auto

lemma MMI_biimpd: assumes A1: "φ --> ( ψ <-> ch )"   
   shows "φ --> ( ψ --> ch )"
   using prems by auto

lemma MMI_orrd: assumes A1: "φ --> ( ¬ ( ψ ) --> ch )"   
   shows "φ --> ( ψ ∨ ch )"
   using prems by auto

lemma MMI_jaoi: assumes A1: "φ --> ψ" and
    A2: "ch --> ψ"   
   shows "( φ ∨ ch ) --> ψ"
   using prems by auto

lemma MMI_oridm: 
   shows "( φ ∨ φ ) <-> φ"
  by auto

lemma MMI_orbi1d: assumes A1: "φ --> ( ψ <-> ch )"   
   shows "φ --> ( ( ψ ∨ ϑ ) <-> ( ch ∨ ϑ ) )"
   using prems by auto

lemma MMI_orbi2d: assumes A1: "φ --> ( ψ <-> ch )"   
   shows "φ --> ( ( ϑ ∨ ψ ) <-> ( ϑ ∨ ch ) )"
   using prems by auto;

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

lemma MMI_3bitr4g: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "ϑ <-> ψ" and
    A3: "τ <-> ch"   
   shows "φ --> ( ϑ <-> τ )"
   using prems by auto

lemma MMI_negbid: assumes A1: "φ --> ( ψ <-> ch )"   
   shows "φ --> ( ¬ ( ψ ) <-> ¬ ( ch ) )"
   using prems by auto

lemma MMI_ioran: 
   shows "¬ ( ( φ ∨ ψ ) ) <-> 
 ( ¬ ( φ ) ∧ ¬ ( ψ ) )"
  by auto

lemma MMI_syl6rbb: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "ch <-> ϑ"   
   shows "φ --> ( ϑ <-> ψ )"
   using prems by auto

lemma MMI_anbi12i: assumes A1: "φ <-> ψ" and
    A2: "ch <-> ϑ"   
   shows "( φ ∧ ch ) <-> ( ψ ∧ ϑ )"
   using prems by auto;

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


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

lemma MMI_imbi2d: assumes A1: "φ --> ( ψ <-> ch )"   
   shows "φ --> ( ( ϑ --> ψ ) <-> ( ϑ --> ch ) )"
   using prems by auto;

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

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

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

lemma MMI_3impia: assumes A1: "( φ ∧ ψ ) --> ( ch --> ϑ )"   
   shows "( φ ∧ ψ ∧ ch ) --> ϑ"
   using prems by auto;

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

lemma MMI_eqneqd: assumes A1: "φ --> ( A = B <-> C = D )"   
   shows "φ --> ( A ≠ B <-> C ≠ D )"
   using prems by auto

lemma MMI_3ad2ant2: assumes A1: "φ --> ch"   
   shows "( ψ ∧ φ ∧ ϑ ) --> ch"
   using prems by auto

lemma MMI_mp3anl3: assumes A1: "ch" and
    A2: "( ( φ ∧ ψ ∧ ch ) ∧ ϑ ) --> τ"   
   shows "( ( φ ∧ ψ ) ∧ ϑ ) --> τ"
   using prems by auto

lemma MMI_bitr4d: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "φ --> ( ϑ <-> ch )"   
   shows "φ --> ( ψ <-> ϑ )"
   using prems by auto

lemma MMI_neeq1d: assumes A1: "φ --> A = B"   
   shows "φ --> ( A ≠ C <-> B ≠ C )"
   using prems by auto;

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

lemma MMI_3anim123i: assumes A1: "φ --> ψ" and
    A2: "ch --> ϑ" and
    A3: "τ --> η"   
   shows "( φ ∧ ch ∧ τ ) --> ( ψ ∧ ϑ ∧ η )"
   using prems by auto

lemma MMI_3exp: assumes A1: "( φ ∧ ψ ∧ ch ) --> ϑ"   
   shows "φ --> ( ψ --> ( ch --> ϑ ) )"
   using prems by auto

lemma MMI_exp4a: assumes A1: "φ --> ( ψ --> ( ( ch ∧ ϑ ) --> τ ) )"   
   shows "φ --> ( ψ --> ( ch --> ( ϑ --> τ ) ) )"
   using prems by auto

lemma MMI_3imp1: assumes A1: "φ --> ( ψ --> ( ch --> ( ϑ --> τ ) ) )"   
   shows "( ( φ ∧ ψ ∧ ch ) ∧ ϑ ) --> τ"
   using prems by auto

lemma MMI_anim1i: assumes A1: "φ --> ψ"   
   shows "( φ ∧ ch ) --> ( ψ ∧ ch )"
   using prems by auto

lemma MMI_3adantl1: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) --> ϑ"   
   shows "( ( τ ∧ φ ∧ ψ ) ∧ ch ) --> ϑ"
   using prems by auto

lemma MMI_3adantl2: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) --> ϑ"   
   shows "( ( φ ∧ τ ∧ ψ ) ∧ ch ) --> ϑ"
   using prems by auto

lemma MMI_3comr: assumes A1: "( φ ∧ ψ ∧ ch ) --> ϑ"   
   shows "( ch ∧ φ ∧ ψ ) --> ϑ"
   using prems by auto;

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

lemma MMI_bitr3: assumes A1: "ψ <-> φ" and
    A2: "ψ <-> ch"   
   shows "φ <-> ch"
   using prems by auto

lemma MMI_anbi12d: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "φ --> ( ϑ <-> τ )"   
   shows "φ --> ( ( ψ ∧ ϑ ) <-> ( ch ∧ τ ) )"
   using prems by auto

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

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

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

lemma MMI_anabsan: assumes A1: "( ( φ ∧ φ ) ∧ ψ ) --> ch"   
   shows "( φ ∧ ψ ) --> ch"
   using prems by auto

lemma MMI_3eqtr4rd: assumes A1: "φ --> A = B" and
    A2: "φ --> C = A" and
    A3: "φ --> D = B"   
   shows "φ --> D = C"
   using prems by auto

lemma MMI_syl3an1: assumes A1: "( φ ∧ ψ ∧ ch ) --> ϑ" and
    A2: "τ --> φ"   
   shows "( τ ∧ ψ ∧ ch ) --> ϑ"
   using prems by auto

lemma MMI_syl3anl2: assumes A1: "( ( φ ∧ ψ ∧ ch ) ∧ ϑ ) --> τ" and
    A2: "η --> ψ"   
   shows "( ( φ ∧ η ∧ ch ) ∧ ϑ ) --> τ"
   using prems by auto;

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


lemma MMI_jca: assumes A1: "φ --> ψ" and
    A2: "φ --> ch"   
   shows "φ --> ( ψ ∧ ch )"
   using prems by auto

lemma MMI_3ad2ant3: assumes A1: "φ --> ch"   
   shows "( ψ ∧ ϑ ∧ φ ) --> ch"
   using prems by auto

lemma MMI_anim2i: assumes A1: "φ --> ψ"   
   shows "( ch ∧ φ ) --> ( ch ∧ ψ )"
   using prems by auto

lemma MMI_ancom: 
   shows "( φ ∧ ψ ) <-> ( ψ ∧ φ )"
  by auto

lemma MMI_anbi1i: assumes Aaa: "φ <-> ψ"   
   shows "( φ ∧ ch ) <-> ( ψ ∧ ch )"
   using prems by auto

lemma MMI_an42: 
   shows "( ( φ ∧ ψ ) ∧ ( ch ∧ ϑ ) ) <-> 
 ( ( φ ∧ ch ) ∧ ( ϑ ∧ ψ ) )"
  by auto

lemma MMI_sylanb: assumes A1: "( φ ∧ ψ ) --> ch" and
    A2: "ϑ <-> φ"   
   shows "( ϑ ∧ ψ ) --> ch"
   using prems by auto

lemma MMI_an4: 
   shows "( ( φ ∧ ψ ) ∧ ( ch ∧ ϑ ) ) <-> 
 ( ( φ ∧ ch ) ∧ ( ψ ∧ ϑ ) )"
  by auto

lemma MMI_syl2anb: assumes A1: "( φ ∧ ψ ) --> ch" and
    A2: "ϑ <-> φ" and
    A3: "τ <-> ψ"   
   shows "( ϑ ∧ τ ) --> ch"
   using prems by auto

lemma MMI_eqtr2d: assumes A1: "φ --> A = B" and
    A2: "φ --> B = C"   
   shows "φ --> C = A"
   using prems by auto

lemma MMI_sylbid: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "φ --> ( ch --> ϑ )"   
   shows "φ --> ( ψ --> ϑ )"
   using prems by auto

lemma MMI_sylanl1: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) --> ϑ" and
    A2: "τ --> φ"   
   shows "( ( τ ∧ ψ ) ∧ ch ) --> ϑ"
   using prems by auto

lemma MMI_sylan2b: assumes A1: "( φ ∧ ψ ) --> ch" and
    A2: "ϑ <-> ψ"   
   shows "( φ ∧ ϑ ) --> ch"
   using prems by auto

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

lemma MMI_ancli: assumes A1: "φ --> ψ"   
   shows "φ --> ( φ ∧ ψ )"
   using prems by auto

lemma MMI_ad2antlr: assumes A1: "φ --> ψ"   
   shows "( ( ch ∧ φ ) ∧ ϑ ) --> ψ"
   using prems by auto

lemma MMI_biimpa: assumes A1: "φ --> ( ψ <-> ch )"   
   shows "( φ ∧ ψ ) --> ch"
   using prems by auto

lemma MMI_sylan2i: assumes A1: "φ --> ( ( ψ ∧ ch ) --> ϑ )" and
    A2: "τ --> ch"   
   shows "φ --> ( ( ψ ∧ τ ) --> ϑ )"
   using prems by auto

lemma MMI_3jca: assumes A1: "φ --> ψ" and
    A2: "φ --> ch" and
    A3: "φ --> ϑ"   
   shows "φ --> ( ψ ∧ ch ∧ ϑ )"
   using prems by auto

lemma MMI_com34: assumes A1: "φ --> ( ψ --> ( ch --> ( ϑ --> τ ) ) )"   
   shows "φ --> ( ψ --> ( ϑ --> ( ch --> τ ) ) )"
   using prems by auto

lemma MMI_imp43: assumes A1: "φ --> ( ψ --> ( ch --> ( ϑ --> τ ) ) )"   
   shows "( ( φ ∧ ψ ) ∧ ( ch ∧ ϑ ) ) --> τ"
   using prems 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 prems by auto

lemma MMI_jctl: assumes A1: "ψ"   
   shows "φ --> ( ψ ∧ φ )"
   using prems by auto

lemma MMI_sylibr: assumes A1: "φ --> ψ" and
    A2: "ch <-> ψ"   
   shows "φ --> ch"
   using prems by auto

lemma MMI_mpanl1: assumes A1: "φ" and
    A2: "( ( φ ∧ ψ ) ∧ ch ) --> ϑ"   
   shows "( ψ ∧ ch ) --> ϑ"
   using prems by auto

lemma MMI_a1i: assumes A1: "φ"   
   shows "ψ --> φ"
   using prems 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 prems by auto

lemma MMI_3adantl3: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) --> ϑ"   
   shows "( ( φ ∧ ψ ∧ τ ) ∧ ch ) --> ϑ"
   using prems by auto

lemma MMI_sylbi: assumes A1: "φ <-> ψ" and
    A2: "ψ --> ch"   
   shows "φ --> ch"
   using prems 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 prems by auto

lemma MMI_mtbir: assumes A1: "¬ ( ψ )" and
    A2: "φ <-> ψ"   
   shows "¬ ( φ )"
   using prems by auto

lemma MMI_mto: assumes A1: "¬ ( ψ )" and
    A2: "φ --> ψ"   
   shows "¬ ( φ )"
   using prems by auto

lemma MMI_df_nel: 
   shows "( A ∉ B <-> ¬ ( A ∈ B ) )"
  by auto

lemma MMI_snid: assumes A1: "A isASet"   
   shows "A ∈ { A }"
   using prems 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 prems 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 prems by auto

lemma MMI_con2i: assumes Aa: "φ --> ¬ ( ψ )"   
   shows "ψ --> ¬ ( φ )"
   using prems by auto

lemma MMI_intnand: assumes A1: "φ --> ¬ ( ψ )"   
   shows "φ --> ¬ ( ( ch ∧ ψ ) )"
   using prems by auto

lemma MMI_intnanrd: assumes A1: "φ --> ¬ ( ψ )"   
   shows "φ --> ¬ ( ( ψ ∧ ch ) )"
   using prems by auto

lemma MMI_biorf: 
   shows "¬ ( φ ) --> ( ψ <-> ( φ ∨ ψ ) )"
  by auto

lemma MMI_bitr2d: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "φ --> ( ch <-> ϑ )"   
   shows "φ --> ( ϑ <-> ψ )"
   using prems 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 prems by auto

lemma MMI_3imtr4d: assumes A1: "φ --> ( ψ --> ch )" and
    A2: "φ --> ( ϑ <-> ψ )" and
    A3: "φ --> ( τ <-> ch )"   
   shows "φ --> ( ϑ --> τ )"
   using prems by auto;

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

lemma MMI_3impdi: assumes A1: "( ( φ ∧ ψ ) ∧ ( φ ∧ ch ) ) --> ϑ"   
   shows "( φ ∧ ψ ∧ ch ) --> ϑ"
   using prems by auto

lemma MMI_bi2anan9: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "ϑ --> ( τ <-> η )"   
   shows "( φ ∧ ϑ ) --> ( ( ψ ∧ τ ) <-> ( ch ∧ η ) )"
   using prems by auto

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

lemma MMI_an1rs: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) --> ϑ"   
   shows "( ( φ ∧ ch ) ∧ ψ ) --> ϑ"
   using prems by auto

(*lemma MMI_ralbidva_original: 
     assumes A1: "( φ ∧ x ∈ A ) --> ( ψ <-> ch )"   
   shows "φ -->  ( ( ∀ x ∈ A . ψ ) <-> ( ∀ x ∈ A . ch ) )"
   using prems by auto;*)

lemma MMI_ralbidva: assumes A1: "∀x. ( φ ∧ x ∈ A ) --> ( ψ(x) <-> ch(x) )"   
   shows "φ -->  ( ( ∀ x ∈ A . ψ(x) ) <-> ( ∀ x ∈ A . ch(x) ) )"
   using prems by auto;

lemma MMI_rexbidva: assumes A1: "∀x. ( φ ∧ x ∈ A ) --> ( ψ(x) <-> ch(x) )"   
   shows "φ -->  ( ( ∃ x ∈ A . ψ(x) ) <-> ( ∃ x ∈ A . ch(x) ) )"
   using prems by auto;

lemma MMI_con2bid: assumes A1: "φ --> ( ψ <-> ¬ ( ch ) )"   
   shows "φ --> ( ch <-> ¬ ( ψ ) )"
   using prems 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 prems StrictOrder_def by auto;

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

lemma MMI_con1bid: assumes A1: "φ --> ( ¬ ( ψ ) <-> ch )"   
   shows "φ --> ( ¬ ( ch ) <-> ψ )"
   using prems 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 prems 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 prems by auto;

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

lemma MMI_orbi1i: assumes A1: "φ <-> ψ"   
   shows "( φ ∨ ch ) <-> ( ψ ∨ ch )"
   using prems by auto;

lemma MMI_syl5rbbr: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "ψ <-> ϑ"   
   shows "φ --> ( ch <-> ϑ )"
   using prems by auto;

lemma MMI_anbi2d: assumes A1: "φ --> ( ψ <-> ch )"   
   shows "φ --> ( ( ϑ ∧ ψ ) <-> ( ϑ ∧ ch ) )"
   using prems by auto;

lemma MMI_ord: assumes A1: "φ --> ( ψ ∨ ch )"   
   shows "φ --> ( ¬ ( ψ ) --> ch )"
   using prems by auto;

lemma MMI_impbid: assumes A1: "φ --> ( ψ --> ch )" and
    A2: "φ --> ( ch --> ψ )"   
   shows "φ --> ( ψ <-> ch )"
   using prems by blast;

lemma MMI_jcad: assumes A1: "φ --> ( ψ --> ch )" and
    A2: "φ --> ( ψ --> ϑ )"   
   shows "φ --> ( ψ --> ( ch ∧ ϑ ) )"
   using prems 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 prems 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 prems by auto

lemma MMI_jaod: assumes A1: "φ --> ( ψ --> ch )" and
    A2: "φ --> ( ϑ --> ch )"   
   shows "φ --> ( ( ψ ∨ ϑ ) --> ch )"
   using prems by auto

lemma MMI_com23: assumes A1: "φ --> ( ψ --> ( ch --> ϑ ) )"   
   shows "φ --> ( ch --> ( ψ --> ϑ ) )"
   using prems 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 prems by auto

lemma MMI_biimpcd: assumes A1: "φ --> ( ψ <-> ch )"   
   shows "ψ --> ( φ --> ch )"
   using prems by auto

lemma MMI_mp2and: assumes A1: "φ --> ψ" and
    A2: "φ --> ch" and
    A3: "φ --> ( ( ψ ∧ ch ) --> ϑ )"   
   shows "φ --> ϑ"
   using prems by auto;

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

lemma MMI_sonr: 
   shows "( R Orders A ∧ B ∈ A ) --> ¬ ( ⟨B,B⟩ ∈ R )"
  using StrictOrder_def by auto;

lemma MMI_orri: assumes A1: "¬ ( φ ) --> ψ"   
   shows "φ ∨ ψ"
   using prems by auto

lemma MMI_mpbiri: assumes Amin: "ch" and
    Amaj: "φ --> ( ψ <-> ch )"   
   shows "φ --> ψ"
   using prems 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> ∈ \<real>*"
  using cxr_def by simp;

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

lemma (in MMIsar0) MMI_mnfxr: 
   shows "\<cmnf> ∈ \<real>*"
  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 prems by auto

lemma MMI_orbi2i: assumes A1: "φ <-> ψ"   
   shows "( ch ∨ φ ) <-> ( ch ∨ ψ )"
   using prems by auto

lemma MMI_3orass: 
   shows "( φ ∨ ψ ∨ ch ) <-> ( φ ∨ ( ψ ∨ ch ) )"
  by auto

lemma MMI_bitr4: assumes A1: "φ <-> ψ" and
    A2: "ch <-> ψ"   
   shows "φ <-> ch"
   using prems 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 prems by auto

lemma MMI_mt2: assumes A1: "ψ" and
    A2: "φ --> ¬ ( ψ )"   
   shows "¬ ( φ )"
   using prems 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 prems 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 prems by auto

lemma MMI_con3d: assumes A1: "φ --> ( ψ --> ch )"   
   shows "φ --> ( ¬ ( ch ) --> ¬ ( ψ ) )"
   using prems 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 prems by auto

lemma MMI_rexbii: assumes A1: "∀x. φ(x) <-> ψ(x)"   
   shows "( ∃ x ∈ A . φ(x) ) <-> ( ∃ x ∈ A . ψ(x) )"
   using prems 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 prems by auto;

(** original lemma MMI_orbi12i: assumes A1: "φ <-> ψ" and
    A2: "ch <-> ϑ"   
   shows "( φ ∨ ch ) <-> ( ψ ∨ ϑ )"
   using prems by auto
*)

lemma MMI_orbi12i: assumes A1: "(∃x. φ(x)) <-> ψ" and
    A2: "(∃x. ch(x)) <-> ϑ"   
   shows "( ∃x. φ(x) ) ∨ (∃x. ch(x) ) <-> ( ψ ∨ ϑ )"
   using prems by auto;

lemma MMI_syl6ib: assumes A1: "φ --> ( ψ --> ch )" and
    A2: "ch <-> ϑ"   
   shows "φ --> ( ψ --> ϑ )"
   using prems by auto

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

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

lemma MMI_pm3_2ni: assumes A1: "¬ ( φ )" and
    A2: "¬ ( ψ )"   
   shows "¬ ( ( φ ∨ ψ ) )"
   using prems 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 prems by auto

lemma MMI_jctr: assumes A1: "ψ"   
   shows "φ --> ( φ ∧ ψ )"
   using prems by auto

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

lemma MMI_3syl: assumes A1: "φ --> ψ" and
    A2: "ψ --> ch" and
    A3: "ch --> ϑ"   
   shows "φ --> ϑ"
   using prems by auto;

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

lemma MMI_mtbird: assumes Amin: "φ --> ¬ ( ch )" and
    Amaj: "φ --> ( ψ <-> ch )"   
   shows "φ --> ¬ ( ψ )"
   using prems by auto

lemma MMI_pm2_21d: assumes A1: "φ --> ¬ ( ψ )"   
   shows "φ --> ( ψ --> ch )"
   using prems by auto

lemma MMI_3jaodan: assumes A1: "( φ ∧ ψ ) --> ch" and
    A2: "( φ ∧ ϑ ) --> ch" and
    A3: "( φ ∧ τ ) --> ch"   
   shows "( φ ∧ ( ψ ∨ ϑ ∨ τ ) ) --> ch"
   using prems by auto

lemma MMI_sylan2br: assumes A1: "( φ ∧ ψ ) --> ch" and
    A2: "ψ <-> ϑ"   
   shows "( φ ∧ ϑ ) --> ch"
   using prems by auto

lemma MMI_3jaoian: assumes A1: "( φ ∧ ψ ) --> ch" and
    A2: "( ϑ ∧ ψ ) --> ch" and
    A3: "( τ ∧ ψ ) --> ch"   
   shows "( ( φ ∨ ϑ ∨ τ ) ∧ ψ ) --> ch"
   using prems by auto

lemma MMI_mtbid: assumes Amin: "φ --> ¬ ( ψ )" and
    Amaj: "φ --> ( ψ <-> ch )"   
   shows "φ --> ¬ ( ch )"
   using prems by auto

lemma MMI_con1d: assumes A1: "φ --> ( ¬ ( ψ ) --> ch )"   
   shows "φ --> ( ¬ ( ch ) --> ψ )"
   using prems by auto

lemma MMI_pm2_21nd: assumes A1: "φ --> ψ"   
   shows "φ --> ( ¬ ( ψ ) --> ch )"
   using prems by auto

lemma MMI_syl3an1b: assumes A1: "( φ ∧ ψ ∧ ch ) --> ϑ" and
    A2: "τ <-> φ"   
   shows "( τ ∧ ψ ∧ ch ) --> ϑ"
   using prems by auto

lemma MMI_adantld: assumes A1: "φ --> ( ψ --> ch )"   
   shows "φ --> ( ( ϑ ∧ ψ ) --> ch )"
   using prems by auto

lemma MMI_adantrd: assumes A1: "φ --> ( ψ --> ch )"   
   shows "φ --> ( ( ψ ∧ ϑ ) --> ch )"
   using prems by auto

lemma MMI_anasss: assumes A1: "( ( φ ∧ ψ ) ∧ ch ) --> ϑ"   
   shows "( φ ∧ ( ψ ∧ ch ) ) --> ϑ"
   using prems by auto

lemma MMI_syl3an3b: assumes A1: "( φ ∧ ψ ∧ ch ) --> ϑ" and
    A2: "τ <-> ch"   
   shows "( φ ∧ ψ ∧ τ ) --> ϑ"
   using prems by auto;

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


lemma MMI_mpbid: assumes Amin: "φ --> ψ" and
    Amaj: "φ --> ( ψ <-> ch )"   
   shows "φ --> ch"
   using prems by auto

lemma MMI_orbi12d: assumes A1: "φ --> ( ψ <-> ch )" and
    A2: "φ --> ( ϑ <-> τ )"   
   shows "φ --> ( ( ψ ∨ ϑ ) <-> ( ch ∨ τ ) )"
   using prems by auto

lemma MMI_ianor: 
   shows "¬ ( φ ∧ ψ ) <-> ¬ φ ∨ ¬ ψ "
  by auto;

lemma MMI_bitr2: assumes A1: "φ <-> ψ" and
    A2: "ψ <-> ch"   
   shows "ch <-> φ"
   using prems by auto

lemma MMI_biimp: assumes A1: "φ <-> ψ"   
   shows "φ --> ψ"
   using prems by auto

lemma MMI_mpan2d: assumes A1: "φ --> ch" and
    A2: "φ --> ( ( ψ ∧ ch ) --> ϑ )"   
   shows "φ --> ( ψ --> ϑ )"
   using prems by auto

lemma MMI_ad2antrr: assumes A1: "φ --> ψ"   
   shows "( ( φ ∧ ch ) ∧ ϑ ) --> ψ"
   using prems by auto

lemma MMI_biimpac: assumes A1: "φ --> ( ψ <-> ch )"   
   shows "( ψ ∧ φ ) --> ch"
   using prems by auto;

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

lemma MMI_con2bii: assumes A1: "φ <-> ¬ ( ψ )"   
   shows "ψ <-> ¬ ( φ )"
   using prems by auto

lemma MMI_pm3_26bd: assumes A1: "φ <-> ( ψ ∧ ch )"   
   shows "φ --> ψ"
   using prems by auto;

end