(* 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)