HomeTheorem List (p. 381 of 489)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 381 of 489) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-30950) |
Hilbert Space Explorer
(30951-32473) |
Users' Mathboxes
(32474-48899) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | maxidlidl 38001 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ∈ (Idl‘𝑅)) | ||
| Theorem | maxidlnr 38002 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ≠ 𝑋) | ||
| Theorem | maxidlmax 38003 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) ∧ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑀 ⊆ 𝐼)) → (𝐼 = 𝑀 ∨ 𝐼 = 𝑋)) | ||
| Theorem | maxidln1 38004 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → ¬ 𝑈 ∈ 𝑀) | ||
| Theorem | maxidln0 38005 | A ring with a maximal ideal is not the zero ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑈 ≠ 𝑍) | ||
| Syntax | cprrng 38006 | Extend class notation with the class of prime rings. |
| class PrRing | ||
| Syntax | cdmn 38007 | Extend class notation with the class of domains. |
| class Dmn | ||
| Definition | df-prrngo 38008 | Define the class of prime rings. A ring is prime if the zero ideal is a prime ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ PrRing = {𝑟 ∈ RingOps ∣ {(GId‘(1st ‘𝑟))} ∈ (PrIdl‘𝑟)} | ||
| Definition | df-dmn 38009 | Define the class of (integral) domains. A domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ Dmn = (PrRing ∩ Com2) | ||
| Theorem | isprrngo 38010 | The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅))) | ||
| Theorem | prrngorngo 38011 | A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ (𝑅 ∈ PrRing → 𝑅 ∈ RingOps) | ||
| Theorem | smprngopr 38012 | A simple ring (one whose only ideals are 0 and 𝑅) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝑅) = {{𝑍}, 𝑋}) → 𝑅 ∈ PrRing) | ||
| Theorem | divrngpr 38013 | A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ (𝑅 ∈ DivRingOps → 𝑅 ∈ PrRing) | ||
| Theorem | isdmn 38014 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ Com2)) | ||
| Theorem | isdmn2 38015 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps)) | ||
| Theorem | dmncrng 38016 | A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ (𝑅 ∈ Dmn → 𝑅 ∈ CRingOps) | ||
| Theorem | dmnrngo 38017 | A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ (𝑅 ∈ Dmn → 𝑅 ∈ RingOps) | ||
| Theorem | flddmn 38018 | A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ (𝐾 ∈ Fld → 𝐾 ∈ Dmn) | ||
| Syntax | cigen 38019 | Extend class notation with the ideal generation function. |
| class IdlGen | ||
| Definition | df-igen 38020* | Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}) | ||
| Theorem | igenval 38021* | The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof shortened by Mario Carneiro, 20-Dec-2013.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) = ∩ {𝑗 ∈ (Idl‘𝑅) ∣ 𝑆 ⊆ 𝑗}) | ||
| Theorem | igenss 38022 | A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (𝑅 IdlGen 𝑆)) | ||
| Theorem | igenidl 38023 | The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) ∈ (Idl‘𝑅)) | ||
| Theorem | igenmin 38024 | The ideal generated by a set is the minimal ideal containing that set. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼) → (𝑅 IdlGen 𝑆) ⊆ 𝐼) | ||
| Theorem | igenidl2 38025 | The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑅 IdlGen 𝐼) = 𝐼) | ||
| Theorem | igenval2 38026* | The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → ((𝑅 IdlGen 𝑆) = 𝐼 ↔ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗)))) | ||
| Theorem | prnc 38027* | A principal ideal (an ideal generated by one element) in a commutative ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋) → (𝑅 IdlGen {𝐴}) = {𝑥 ∈ 𝑋 ∣ ∃𝑦 ∈ 𝑋 𝑥 = (𝑦𝐻𝐴)}) | ||
| Theorem | isfldidl 38028 | Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝐾) & ⊢ 𝐻 = (2nd ‘𝐾) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ (Idl‘𝐾) = {{𝑍}, 𝑋})) | ||
| Theorem | isfldidl2 38029 | Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝐾) & ⊢ 𝐻 = (2nd ‘𝐾) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ CRingOps ∧ 𝑋 ≠ {𝑍} ∧ (Idl‘𝐾) = {{𝑍}, 𝑋})) | ||
| Theorem | ispridlc 38030* | The predicate "is a prime ideal". Alternate definition for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))))) | ||
| Theorem | pridlc 38031 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → (𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃)) | ||
| Theorem | pridlc2 38032 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → 𝐵 ∈ 𝑃) | ||
| Theorem | pridlc3 38033 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ (𝑋 ∖ 𝑃))) → (𝐴𝐻𝐵) ∈ (𝑋 ∖ 𝑃)) | ||
| Theorem | isdmn3 38034* | The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍)))) | ||
| Theorem | dmnnzd 38035 | A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) = 𝑍)) → (𝐴 = 𝑍 ∨ 𝐵 = 𝑍)) | ||
| Theorem | dmncan1 38036 | Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → ((𝐴𝐻𝐵) = (𝐴𝐻𝐶) → 𝐵 = 𝐶)) | ||
| Theorem | dmncan2 38037 | Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐶 ≠ 𝑍) → ((𝐴𝐻𝐶) = (𝐵𝐻𝐶) → 𝐴 = 𝐵)) | ||
The results in this section are mostly meant for being used by automatic proof building programs. As a result, they might appear less useful or meaningful than others to human beings. | ||
| Theorem | efald2 38038 | A proof by contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (¬ 𝜑 → ⊥) ⇒ ⊢ 𝜑 | ||
| Theorem | notbinot1 38039 | Simplification rule of negation across a biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (¬ (¬ 𝜑 ↔ 𝜓) ↔ (𝜑 ↔ 𝜓)) | ||
| Theorem | bicontr 38040 | Biconditional of its own negation is a contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ ((¬ 𝜑 ↔ 𝜑) ↔ ⊥) | ||
| Theorem | impor 38041 | An equivalent formula for implying a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ ((𝜑 → (𝜓 ∨ 𝜒)) ↔ ((¬ 𝜑 ∨ 𝜓) ∨ 𝜒)) | ||
| Theorem | orfa 38042 | The falsum ⊥ can be removed from a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ ((𝜑 ∨ ⊥) ↔ 𝜑) | ||
| Theorem | notbinot2 38043 | Commutation rule between negation and biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (¬ (𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ 𝜓)) | ||
| Theorem | biimpor 38044 | A rewriting rule for biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((¬ 𝜑 ↔ 𝜓) ∨ 𝜒)) | ||
| Theorem | orfa1 38045 | Add a contradicting disjunct to an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∨ ⊥) → 𝜓) | ||
| Theorem | orfa2 38046 | Remove a contradicting disjunct from an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (𝜑 → ⊥) ⇒ ⊢ ((𝜑 ∨ 𝜓) → 𝜓) | ||
| Theorem | bifald 38047 | Infer the equivalence to a contradiction from a negation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ ⊥)) | ||
| Theorem | orsild 38048 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
| Theorem | orsird 38049 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
| Theorem | cnf1dd 38050 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
| ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) & ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
| Theorem | cnf2dd 38051 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
| ⊢ (𝜑 → (𝜓 → ¬ 𝜃)) & ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
| Theorem | cnfn1dd 38052 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → (¬ 𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
| Theorem | cnfn2dd 38053 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
| ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → (𝜒 ∨ ¬ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
| Theorem | or32dd 38054 | A rearrangement of disjuncts, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
| ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃) ∨ 𝜏))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) ∨ 𝜃))) | ||
| Theorem | notornotel1 38055 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
| ⊢ (𝜑 → ¬ (¬ 𝜓 ∨ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | notornotel2 38056 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
| ⊢ (𝜑 → ¬ (𝜓 ∨ ¬ 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
| Theorem | contrd 38057 | A proof by contradiction, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
| ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) & ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | an12i 38058 | An inference from commuting operands in a chain of conjunctions. (Contributed by Giovanni Mascellani, 22-May-2019.) |
| ⊢ (𝜑 ∧ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 ∧ (𝜑 ∧ 𝜒)) | ||
| Theorem | exmid2 38059 | An excluded middle law. (Contributed by Giovanni Mascellani, 23-May-2019.) |
| ⊢ ((𝜓 ∧ 𝜑) → 𝜒) & ⊢ ((¬ 𝜓 ∧ 𝜂) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜂) → 𝜒) | ||
| Theorem | selconj 38060 | An inference for selecting one of a list of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.) |
| ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ ((𝜂 ∧ 𝜑) ↔ (𝜓 ∧ (𝜂 ∧ 𝜒))) | ||
| Theorem | truconj 38061 | Add true as a conjunct. (Contributed by Giovanni Mascellani, 23-May-2019.) |
| ⊢ (𝜑 ↔ (⊤ ∧ 𝜑)) | ||
| Theorem | orel 38062 | An inference for disjunction elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
| ⊢ ((𝜓 ∧ 𝜂) → 𝜃) & ⊢ ((𝜒 ∧ 𝜌) → 𝜃) & ⊢ (𝜑 → (𝜓 ∨ 𝜒)) ⇒ ⊢ ((𝜑 ∧ (𝜂 ∧ 𝜌)) → 𝜃) | ||
| Theorem | negel 38063 | An inference for negation elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
| ⊢ (𝜓 → 𝜒) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ⊥) | ||
| Theorem | botel 38064 | An inference for bottom elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
| ⊢ (𝜑 → ⊥) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | tradd 38065 | Add top ad a conjunct. (Contributed by Giovanni Mascellani, 24-May-2019.) |
| ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ (⊤ ∧ 𝜓)) | ||
| Theorem | gm-sbtru 38066 | Substitution does not change truth. (Contributed by Giovanni Mascellani, 24-May-2019.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]⊤ ↔ ⊤) | ||
| Theorem | sbfal 38067 | Substitution does not change falsity. (Contributed by Giovanni Mascellani, 24-May-2019.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]⊥ ↔ ⊥) | ||
| Theorem | sbcani 38068 | Distribution of class substitution over conjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
| ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒) & ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂) ⇒ ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ (𝜒 ∧ 𝜂)) | ||
| Theorem | sbcori 38069 | Distribution of class substitution over disjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
| ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒) & ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂) ⇒ ⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ (𝜒 ∨ 𝜂)) | ||
| Theorem | sbcimi 38070 | Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
| ⊢ 𝐴 ∈ V & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒) & ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂) ⇒ ⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ (𝜒 → 𝜂)) | ||
| Theorem | sbcni 38071 | Move class substitution inside a negation, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
| ⊢ 𝐴 ∈ V & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ 𝜓) | ||
| Theorem | sbali 38072 | Discard class substitution in a universal quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]∀𝑥𝜑 ↔ ∀𝑥𝜑) | ||
| Theorem | sbexi 38073 | Discard class substitution in an existential quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]∃𝑥𝜑 ↔ ∃𝑥𝜑) | ||
| Theorem | sbcalf 38074* | Move universal quantifier in and out of class substitution, with an explicit nonfree variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.) |
| ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ ([𝐴 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦[𝐴 / 𝑥]𝜑) | ||
| Theorem | sbcexf 38075* | Move existential quantifier in and out of class substitution, with an explicit nonfree variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.) |
| ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ ([𝐴 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦[𝐴 / 𝑥]𝜑) | ||
| Theorem | sbcalfi 38076* | Move universal quantifier in and out of class substitution, with an explicit nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
| ⊢ Ⅎ𝑦𝐴 & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦𝜓) | ||
| Theorem | sbcexfi 38077* | Move existential quantifier in and out of class substitution, with an explicit nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
| ⊢ Ⅎ𝑦𝐴 & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦𝜓) | ||
| Theorem | spsbcdi 38078 | A lemma for eliminating a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
| ⊢ 𝐴 ∈ V & ⊢ (𝜑 → ∀𝑥𝜒) & ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | alrimii 38079* | A lemma for introducing a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
| ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝜓) & ⊢ ([𝑦 / 𝑥]𝜒 ↔ 𝜓) & ⊢ Ⅎ𝑦𝜒 ⇒ ⊢ (𝜑 → ∀𝑥𝜒) | ||
| Theorem | spesbcdi 38080 | A lemma for introducing an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
| ⊢ (𝜑 → 𝜓) & ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥𝜒) | ||
| Theorem | exlimddvf 38081 | A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019.) |
| ⊢ (𝜑 → ∃𝑥𝜃) & ⊢ Ⅎ𝑥𝜓 & ⊢ ((𝜃 ∧ 𝜓) → 𝜒) & ⊢ Ⅎ𝑥𝜒 ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
| Theorem | exlimddvfi 38082 | A lemma for eliminating an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.) |
| ⊢ (𝜑 → ∃𝑥𝜃) & ⊢ Ⅎ𝑦𝜃 & ⊢ Ⅎ𝑦𝜓 & ⊢ ([𝑦 / 𝑥]𝜃 ↔ 𝜂) & ⊢ ((𝜂 ∧ 𝜓) → 𝜒) & ⊢ Ⅎ𝑦𝜒 ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
| Theorem | sbceq1ddi 38083 | A lemma for eliminating inequality, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝜃) & ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜃) & ⊢ ([𝐵 / 𝑥]𝜒 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜂) | ||
| Theorem | sbccom2lem 38084* | Lemma for sbccom2 38085. (Contributed by Giovanni Mascellani, 31-May-2019.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
| Theorem | sbccom2 38085* | Commutative law for double class substitution. (Contributed by Giovanni Mascellani, 31-May-2019.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
| Theorem | sbccom2f 38086* | Commutative law for double class substitution, with nonfree variable condition. (Contributed by Giovanni Mascellani, 31-May-2019.) |
| ⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
| Theorem | sbccom2fi 38087* | Commutative law for double class substitution, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.) |
| ⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑦𝐴 & ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜓) | ||
| Theorem | csbcom2fi 38088* | Commutative law for double class substitution in a class, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.) |
| ⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑦𝐴 & ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 & ⊢ ⦋𝐴 / 𝑥⦌𝐷 = 𝐸 ⇒ ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐸 | ||
A collection of Tseitin axioms used to convert a wff to Conjunctive Normal Form. | ||
| Theorem | fald 38089 | Refutation of falsity, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
| ⊢ (𝜃 → ¬ ⊥) | ||
| Theorem | tsim1 38090 | A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
| ⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 → 𝜓))) | ||
| Theorem | tsim2 38091 | A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
| ⊢ (𝜃 → (𝜑 ∨ (𝜑 → 𝜓))) | ||
| Theorem | tsim3 38092 | A Tseitin axiom for logical implication, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
| ⊢ (𝜃 → (¬ 𝜓 ∨ (𝜑 → 𝜓))) | ||
| Theorem | tsbi1 38093 | A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
| ⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ↔ 𝜓))) | ||
| Theorem | tsbi2 38094 | A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
| ⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ (𝜑 ↔ 𝜓))) | ||
| Theorem | tsbi3 38095 | A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
| ⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓))) | ||
| Theorem | tsbi4 38096 | A Tseitin axiom for logical biconditional, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
| ⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓))) | ||
| Theorem | tsxo1 38097 | A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
| ⊢ (𝜃 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓))) | ||
| Theorem | tsxo2 38098 | A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
| ⊢ (𝜃 → ((𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ⊻ 𝜓))) | ||
| Theorem | tsxo3 38099 | A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
| ⊢ (𝜃 → ((𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ⊻ 𝜓))) | ||
| Theorem | tsxo4 38100 | A Tseitin axiom for logical exclusive disjunction, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
| ⊢ (𝜃 → ((¬ 𝜑 ∨ 𝜓) ∨ (𝜑 ⊻ 𝜓))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |