P. 3 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 201-300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	peirce 201	Peirce's axiom. A non-intuitionistic implication-only statement. Added to intuitionistic (implicational) propositional calculus, it gives classical (implicational) propositional calculus. For another non-intuitionistic positive statement, see curryax 891. When ⊥ is substituted for 𝜓, then this becomes the Clavius law pm2.18 128. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 9-Oct-2012.)
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
Theorem	looinv 202	The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. Using dfor2 899, we can see that this essentially expresses "disjunction commutes". Theorem *2.69 of [WhiteheadRussell] p. 108. It is a special instance of the axiom "Roll", see peirceroll 85. (Contributed by NM, 12-Aug-2004.)
⊢ (((𝜑 → 𝜓) → 𝜓) → ((𝜓 → 𝜑) → 𝜑))
Theorem	bijust0 203	A self-implication (see id 22) does not imply its own negation. The justification theorem bijust 204 is one of its instances. (Contributed by NM, 11-May-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.) Extract bijust0 203 from proof of bijust 204. (Revised by BJ, 19-Mar-2020.)
⊢ ¬ ((𝜑 → 𝜑) → ¬ (𝜑 → 𝜑))
Theorem	bijust 204	Theorem used to justify the definition of the biconditional df-bi 206. Instance of bijust0 203. (Contributed by NM, 11-May-1999.)
⊢ ¬ ((¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))))
1.2.5  Logical equivalence Definition df-bi 206 in this section is our first definition, which introduces and defines the biconditional connective ↔ used to denote logical equivalence. We define a wff of the form (𝜑 ↔ 𝜓) as an abbreviation for ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)). Unlike most traditional developments, we have chosen not to have a separate symbol such as "Df." to mean "is defined as". Instead, we will later use the biconditional connective for this purpose (df-an 397 is its first use), as it allows us to use logic to manipulate definitions directly. This greatly simplifies many proofs since it eliminates the need for a separate mechanism for introducing and eliminating definitions. A note on definitions: definitions are required to be eliminable (that is, a theorem stated in terms of the defined symbol can also be stated without it) and conservative (that is, a theorem whose statement does not contain the defined symbol can be proved without using that definition). This means that a definition does not increase the expressive power nor the deductive power, respectively, of a theory. On the other hand, definitions are often useful to write shorter proofs, so in (i)set.mm we will generally not try to avoid them. This is why, for instance, some theorems which do not contain disjunction in their statement are placed after the section on disjunction because a shorter proof using disjunction is possible.
Syntax	wb 205	Extend wff definition to include the biconditional connective.
wff (𝜑 ↔ 𝜓)
Definition	df-bi 206	Define the biconditional (logical "iff" or "if and only if"), also called biimplication. Definition df-bi 206 in this section is our first definition, which introduces and defines the biconditional connective ↔. We define a wff of the form (𝜑 ↔ 𝜓) as an abbreviation for ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)). Unlike most traditional developments, we have chosen not to have a separate symbol such as "Df." to mean "is defined as". Instead, we will later use the biconditional connective for this purpose (df-or 845 is its first use), as it allows us to use logic to manipulate definitions directly. This greatly simplifies many proofs since it eliminates the need for a separate mechanism for introducing and eliminating definitions. Of course, we cannot use this mechanism to define the biconditional itself, since it hasn't been introduced yet. Instead, we use a more general form of definition, described as follows. In its most general form, a definition is simply an assertion that introduces a new symbol (or a new combination of existing symbols, as in df-3an 1088) that is eliminable and does not strengthen the existing language. The latter requirement means that the set of provable statements not containing the new symbol (or new combination) should remain exactly the same after the definition is introduced. Our definition of the biconditional may look unusual compared to most definitions, but it strictly satisfies these requirements. The justification for our definition is that if we mechanically replace (𝜑 ↔ 𝜓) (the definiendum i.e. the thing being defined) with ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) (the definiens i.e. the defining expression) in the definition, the definition becomes the previously proved theorem bijust 204. It is impossible to use df-bi 206 to prove any statement expressed in the original language that can't be proved from the original axioms, because if we simply replace each instance of df-bi 206 in the proof with the corresponding bijust 204 instance, we will end up with a proof from the original axioms. Note that from Metamath's point of view, a definition is just another axiom - i.e. an assertion we claim to be true - but from our high level point of view, we are not strengthening the language. To indicate this fact, we prefix definition labels with "df-" instead of "ax-". (This prefixing is an informal convention that means nothing to the Metamath proof verifier; it is just a naming convention for human readability.) After we define the constant true ⊤ (df-tru 1542) and the constant false ⊥ (df-fal 1552), we will be able to prove these truth table values: ((⊤ ↔ ⊤) ↔ ⊤) (trubitru 1568), ((⊤ ↔ ⊥) ↔ ⊥) (trubifal 1570), ((⊥ ↔ ⊤) ↔ ⊥) (falbitru 1569), and ((⊥ ↔ ⊥) ↔ ⊤) (falbifal 1571). See dfbi1 212, dfbi2 475, and dfbi3 1047 for theorems suggesting typical textbook definitions of ↔, showing that our definition has the properties we expect. Theorem dfbi1 212 is particularly useful if we want to eliminate ↔ from an expression to convert it to primitives. Theorem dfbi 476 shows this definition rewritten in an abbreviated form after conjunction is introduced, for easier understanding. Contrast with ∨ (df-or 845), → (wi 4), ⊼ (df-nan 1487), and ⊻ (df-xor 1507). In some sense ↔ returns true if two truth values are equal; = (df-cleq 2730) returns true if two classes are equal. (Contributed by NM, 27-Dec-1992.)
⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
Theorem	impbi 207	Property of the biconditional connective. (Contributed by NM, 11-May-1999.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓)))
Theorem	impbii 208	Infer an equivalence from an implication and its converse. Inference associated with impbi 207. (Contributed by NM, 29-Dec-1992.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜑)    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	impbidd 209	Deduce an equivalence from two implications. Double deduction associated with impbi 207 and impbii 208. Deduction associated with impbid 211. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
Theorem	impbid21d 210	Deduce an equivalence from two implications. (Contributed by Wolf Lammen, 12-May-2013.)
⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → (𝜃 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
Theorem	impbid 211	Deduce an equivalence from two implications. Deduction associated with impbi 207 and impbii 208. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 210. (Revised by Wolf Lammen, 3-Nov-2012.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	dfbi1 212	Relate the biconditional connective to primitive connectives. See dfbi1ALT 213 for an unusual version proved directly from axioms. (Contributed by NM, 29-Dec-1992.)
⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
Theorem	dfbi1ALT 213	Alternate proof of dfbi1 212. This proof, discovered by Gregory Bush on 8-Mar-2004, has several curious properties. First, it has only 17 steps directly from the axioms and df-bi 206, compared to over 800 steps were the proof of dfbi1 212 expanded into axioms. Second, step 2 demands only the property of "true"; any axiom (or theorem) could be used. It might be thought, therefore, that it is in some sense redundant, but in fact no proof is shorter than this (measured by number of steps). Third, it illustrates how intermediate steps can "blow up" in size even in short proofs. Fourth, the compressed proof is only 182 bytes (or 17 bytes in D-proof notation), but the generated web page is over 200kB with intermediate steps that are essentially incomprehensible to humans (other than Gregory Bush). If there were an obfuscated code contest for proofs, this would be a contender. This "blowing up" and incomprehensibility of the intermediate steps vividly demonstrate the advantages of using many layered intermediate theorems, since each theorem is easier to understand. (Contributed by Gregory Bush, 10-Mar-2004.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
Theorem	biimp 214	Property of the biconditional connective. (Contributed by NM, 11-May-1999.)
⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))
Theorem	biimpi 215	Infer an implication from a logical equivalence. Inference associated with biimp 214. (Contributed by NM, 29-Dec-1992.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	sylbi 216	A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	sylib 217	A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	sylbb 218	A mixed syllogism inference from two biconditionals. (Contributed by BJ, 30-Mar-2019.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	biimpr 219	Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))
Theorem	bicom1 220	Commutative law for the biconditional. (Contributed by Wolf Lammen, 10-Nov-2012.)
⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
Theorem	bicom 221	Commutative law for the biconditional. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.)
⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))
Theorem	bicomd 222	Commute two sides of a biconditional in a deduction. (Contributed by NM, 14-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ↔ 𝜓))
Theorem	bicomi 223	Inference from commutative law for logical equivalence. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜓 ↔ 𝜑)
Theorem	impbid1 224	Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜒 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	impbid2 225	Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)
⊢ (𝜓 → 𝜒)    &   ⊢ (𝜑 → (𝜒 → 𝜓))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	impcon4bid 226	A variation on impbid 211 with contraposition. (Contributed by Jeff Hankins, 3-Jul-2009.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	biimpri 227	Infer a converse implication from a logical equivalence. Inference associated with biimpr 219. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 16-Sep-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (𝜓 → 𝜑)
Theorem	biimpd 228	Deduce an implication from a logical equivalence. Deduction associated with biimp 214 and biimpi 215. (Contributed by NM, 11-Jan-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	mpbi 229	An inference from a biconditional, related to modus ponens. (Contributed by NM, 11-May-1993.)
⊢ 𝜑    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ 𝜓
Theorem	mpbir 230	An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992.)
⊢ 𝜓    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ 𝜑
Theorem	mpbid 231	A deduction from a biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	mpbii 232	An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
⊢ 𝜓    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	sylibr 233	A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	sylbir 234	A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	sylbbr 235	A mixed syllogism inference from two biconditionals. Note on the various syllogism-like statements in set.mm. The hypothetical syllogism syl 17 infers an implication from two implications (and there are 3syl 18 and 4syl 19 for chaining more inferences). There are four inferences inferring an implication from one implication and one biconditional: sylbi 216, sylib 217, sylbir 234, sylibr 233; four inferences inferring an implication from two biconditionals: sylbb 218, sylbbr 235, sylbb1 236, sylbb2 237; four inferences inferring a biconditional from two biconditionals: bitri 274, bitr2i 275, bitr3i 276, bitr4i 277 (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, syld 47, syl5 34, syl6 35, mpbid 231, bitrd 278, bitrid 282, bitrdi 287 and variants. (Contributed by BJ, 21-Apr-2019.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (𝜒 → 𝜑)
Theorem	sylbb1 236	A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜑 ↔ 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	sylbb2 237	A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	sylibd 238	A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	sylbid 239	A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	mpbidi 240	A deduction from a biconditional, related to modus ponens. (Contributed by NM, 9-Aug-1994.)
⊢ (𝜃 → (𝜑 → 𝜓))    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜃 → (𝜑 → 𝜒))
Theorem	syl5bi 241	A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 12-Jan-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 → (𝜓 → 𝜃))    ⇒   ⊢ (𝜒 → (𝜑 → 𝜃))
Theorem	syl5bir 242	A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (𝜒 → (𝜓 → 𝜃))    ⇒   ⊢ (𝜒 → (𝜑 → 𝜃))
Theorem	syl5ib 243	A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜒 → (𝜑 → 𝜃))
Theorem	syl5ibcom 244	A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜃))
Theorem	syl5ibr 245	A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)
⊢ (𝜑 → 𝜃)    &   ⊢ (𝜒 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜒 → (𝜑 → 𝜓))
Theorem	syl5ibrcom 246	A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)
⊢ (𝜑 → 𝜃)    &   ⊢ (𝜒 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜓))
Theorem	biimprd 247	Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 219 and biimpri 227. (Contributed by NM, 11-Jan-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜓))
Theorem	biimpcd 248	Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜓 → (𝜑 → 𝜒))
Theorem	biimprcd 249	Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜒 → (𝜑 → 𝜓))
Theorem	syl6ib 250	A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	syl6ibr 251	A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 10-Jan-1993.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 ↔ 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	syl6bi 252	A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	syl6bir 253	A mixed syllogism inference. (Contributed by NM, 18-May-1994.)
⊢ (𝜑 → (𝜒 ↔ 𝜓))    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	syl7bi 254	A mixed syllogism inference from a doubly nested implication and a biconditional. (Contributed by NM, 14-May-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 → (𝜃 → (𝜓 → 𝜏)))    ⇒   ⊢ (𝜒 → (𝜃 → (𝜑 → 𝜏)))
Theorem	syl8ib 255	A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜃 ↔ 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
Theorem	mpbird 256	A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	mpbiri 257	An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
⊢ 𝜒    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	sylibrd 258	A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	sylbird 259	A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
⊢ (𝜑 → (𝜒 ↔ 𝜓))    &   ⊢ (𝜑 → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜃))
Theorem	biid 260	Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117. This is part of Frege's eighth axiom per Proposition 54 of [Frege1879] p. 50; see also eqid 2738. (Contributed by NM, 2-Jun-1993.)
⊢ (𝜑 ↔ 𝜑)
Theorem	biidd 261	Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜓))
Theorem	pm5.1im 262	Two propositions are equivalent if they are both true. Closed form of 2th 263. Equivalent to a biimp 214-like version of the xor-connective. This theorem stays true, no matter how you permute its operands. This is evident from its sharper version (𝜑 ↔ (𝜓 ↔ (𝜑 ↔ 𝜓))). (Contributed by Wolf Lammen, 12-May-2013.)
⊢ (𝜑 → (𝜓 → (𝜑 ↔ 𝜓)))
Theorem	2th 263	Two truths are equivalent. (Contributed by NM, 18-Aug-1993.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	2thd 264	Two truths are equivalent. Deduction form. (Contributed by NM, 3-Jun-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	monothetic 265	Two self-implications (see id 22) are equivalent. This theorem, rather trivial in our axiomatization, is (the biconditional form of) a standard axiom for monothetic BCI logic. This is the most general theorem of which trujust 1541 is an instance. Relatedly, this would be the justification theorem if the definition of ⊤ were dftru2 1544. (Contributed by BJ, 7-Sep-2022.)
⊢ ((𝜑 → 𝜑) ↔ (𝜓 → 𝜓))
Theorem	ibi 266	Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003.)
⊢ (𝜑 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	ibir 267	Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.)
⊢ (𝜑 → (𝜓 ↔ 𝜑))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	ibd 268	Deduction that converts a biconditional implied by one of its arguments, into an implication. Deduction associated with ibi 266. (Contributed by NM, 26-Jun-2004.)
⊢ (𝜑 → (𝜓 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	pm5.74 269	Distribution of implication over biconditional. Theorem *5.74 of [WhiteheadRussell] p. 126. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 11-Apr-2013.)
⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒)))
Theorem	pm5.74i 270	Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
Theorem	pm5.74ri 271	Distribution of implication over biconditional (reverse inference form). (Contributed by NM, 1-Aug-1994.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	pm5.74d 272	Distribution of implication over biconditional (deduction form). (Contributed by NM, 21-Mar-1996.)
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))
Theorem	pm5.74rd 273	Distribution of implication over biconditional (deduction form). (Contributed by NM, 19-Mar-1997.)
⊢ (𝜑 → ((𝜓 → 𝜒) ↔ (𝜓 → 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))
Theorem	bitri 274	An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (𝜑 ↔ 𝜒)
Theorem	bitr2i 275	An inference from transitive law for logical equivalence. (Contributed by NM, 12-Mar-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (𝜒 ↔ 𝜑)
Theorem	bitr3i 276	An inference from transitive law for logical equivalence. (Contributed by NM, 2-Jun-1993.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (𝜑 ↔ 𝜒)
Theorem	bitr4i 277	An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ 𝜒)
Theorem	bitrd 278	Deduction form of bitri 274. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
Theorem	bitr2d 279	Deduction form of bitr2i 275. (Contributed by NM, 9-Jun-2004.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜓))
Theorem	bitr3d 280	Deduction form of bitr3i 276. (Contributed by NM, 14-May-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 ↔ 𝜃))
Theorem	bitr4d 281	Deduction form of bitr4i 277. (Contributed by NM, 30-Jun-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
Theorem	bitrid 282	A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜒 → (𝜑 ↔ 𝜃))
Theorem	syl5bb 283	A syllogism inference from two biconditionals. This is in the process of being renamed to bitrid 282 (New usages should use bitrid 282). (Contributed by NM, 12-Mar-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜒 → (𝜑 ↔ 𝜃))
Theorem	bitr2id 284	A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜒 → (𝜃 ↔ 𝜑))
Theorem	bitr3id 285	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (𝜒 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜒 → (𝜑 ↔ 𝜃))
Theorem	bitr3di 286	A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜓 ↔ 𝜃)    ⇒   ⊢ (𝜑 → (𝜒 ↔ 𝜃))
Theorem	bitrdi 287	A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
Theorem	bitr2di 288	A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜓))
Theorem	bitr4di 289	A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 ↔ 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
Theorem	bitr4id 290	A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
⊢ (𝜓 ↔ 𝜒)    &   ⊢ (𝜑 → (𝜃 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
Theorem	3imtr3i 291	A mixed syllogism inference, useful for removing a definition from both sides of an implication. (Contributed by NM, 10-Aug-1994.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 ↔ 𝜒)    &   ⊢ (𝜓 ↔ 𝜃)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	3imtr4i 292	A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	3imtr3d 293	More general version of 3imtr3i 291. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜃 → 𝜏))
Theorem	3imtr4d 294	More general version of 3imtr4i 292. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜓))    &   ⊢ (𝜑 → (𝜏 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜃 → 𝜏))
Theorem	3imtr3g 295	More general version of 3imtr3i 291. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 ↔ 𝜃)    &   ⊢ (𝜒 ↔ 𝜏)    ⇒   ⊢ (𝜑 → (𝜃 → 𝜏))
Theorem	3imtr4g 296	More general version of 3imtr4i 292. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜒)    ⇒   ⊢ (𝜑 → (𝜃 → 𝜏))
Theorem	3bitri 297	A chained inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜑 ↔ 𝜃)
Theorem	3bitrri 298	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜃 ↔ 𝜑)
Theorem	3bitr2i 299	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜑 ↔ 𝜃)
Theorem	3bitr2ri 300	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜃 ↔ 𝜑)