P. 2 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 101-200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pm2.24 101	Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
⊢ (φ → (¬ φ → ψ))
Theorem	pm2.18 102	Proof by contradiction. Theorem *2.18 of [WhiteheadRussell] p. 103. Also called the Law of Clavius. (Contributed by NM, 5-Aug-1993.)
⊢ ((¬ φ → φ) → φ)
Theorem	pm2.18d 103	Deduction based on reductio ad absurdum. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (φ → (¬ ψ → ψ))    ⇒   ⊢ (φ → ψ)
Theorem	notnot2 104	Converse of double negation. Theorem *2.14 of [WhiteheadRussell] p. 102. (Contributed by NM, 5-Aug-1993.) (Proof shortened by David Harvey, 5-Sep-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ (¬ ¬ φ → φ)
Theorem	notnotrd 105	Deduction converting double-negation into the original wff, aka the double negation rule. A translation of natural deduction rule ¬ ¬ -C, Gamma ⊢ ¬ ¬ ψ => Gamma ⊢ ψ; see natded in set.mm. This is definition NNC in [Pfenning] p. 17. This rule is valid in classical logic (which MPE uses), but not intuitionistic logic. (Contributed by DAW, 8-Feb-2017.)
⊢ (φ → ¬ ¬ ψ)    ⇒   ⊢ (φ → ψ)
Theorem	notnotri 106	Inference from double negation. (Contributed by NM, 27-Feb-2008.)
⊢ ¬ ¬ φ    ⇒   ⊢ φ
Theorem	con2d 107	A contraposition deduction. (Contributed by NM, 19-Aug-1993.)
⊢ (φ → (ψ → ¬ χ))    ⇒   ⊢ (φ → (χ → ¬ ψ))
Theorem	con2 108	Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
⊢ ((φ → ¬ ψ) → (ψ → ¬ φ))
Theorem	mt2d 109	Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
⊢ (φ → χ)    &   ⊢ (φ → (ψ → ¬ χ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	mt2i 110	Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
⊢ χ    &   ⊢ (φ → (ψ → ¬ χ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	nsyl3 111	A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
⊢ (φ → ¬ ψ)    &   ⊢ (χ → ψ)    ⇒   ⊢ (χ → ¬ φ)
Theorem	con2i 112	A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.)
⊢ (φ → ¬ ψ)    ⇒   ⊢ (ψ → ¬ φ)
Theorem	nsyl 113	A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
⊢ (φ → ¬ ψ)    &   ⊢ (χ → ψ)    ⇒   ⊢ (φ → ¬ χ)
Theorem	notnot1 114	Converse of double negation. Theorem *2.12 of [WhiteheadRussell] p. 101. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
⊢ (φ → ¬ ¬ φ)
Theorem	notnoti 115	Infer double negation. (Contributed by NM, 27-Feb-2008.)
⊢ φ    ⇒   ⊢ ¬ ¬ φ
Theorem	con1d 116	A contraposition deduction. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (¬ ψ → χ))    ⇒   ⊢ (φ → (¬ χ → ψ))
Theorem	mt3d 117	Modus tollens deduction. (Contributed by NM, 26-Mar-1995.)
⊢ (φ → ¬ χ)    &   ⊢ (φ → (¬ ψ → χ))    ⇒   ⊢ (φ → ψ)
Theorem	mt3i 118	Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
⊢ ¬ χ    &   ⊢ (φ → (¬ ψ → χ))    ⇒   ⊢ (φ → ψ)
Theorem	nsyl2 119	A negated syllogism inference. (Contributed by NM, 26-Jun-1994.)
⊢ (φ → ¬ ψ)    &   ⊢ (¬ χ → ψ)    ⇒   ⊢ (φ → χ)
Theorem	con1 120	Contraposition. Theorem *2.15 of [WhiteheadRussell] p. 102. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
⊢ ((¬ φ → ψ) → (¬ ψ → φ))
Theorem	con1i 121	A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 19-Jun-2013.)
⊢ (¬ φ → ψ)    ⇒   ⊢ (¬ ψ → φ)
Theorem	con4i 122	Inference rule derived from Axiom ax-3 8. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Jun-2013.)
⊢ (¬ φ → ¬ ψ)    ⇒   ⊢ (ψ → φ)
Theorem	pm2.21i 123	A contradiction implies anything. Inference from pm2.21 100. (Contributed by NM, 16-Sep-1993.)
⊢ ¬ φ    ⇒   ⊢ (φ → ψ)
Theorem	pm2.24ii 124	A contradiction implies anything. Inference from pm2.24 101. (Contributed by NM, 27-Feb-2008.)
⊢ φ    &   ⊢ ¬ φ    ⇒   ⊢ ψ
Theorem	con3d 125	A contraposition deduction. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (¬ χ → ¬ ψ))
Theorem	con3 126	Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)
⊢ ((φ → ψ) → (¬ ψ → ¬ φ))
Theorem	con3i 127	A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)
⊢ (φ → ψ)    ⇒   ⊢ (¬ ψ → ¬ φ)
Theorem	con3rr3 128	Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (¬ χ → (φ → ¬ ψ))
Theorem	mt4 129	The rule of modus tollens. (Contributed by Wolf Lammen, 12-May-2013.)
⊢ φ    &   ⊢ (¬ ψ → ¬ φ)    ⇒   ⊢ ψ
Theorem	mt4d 130	Modus tollens deduction. (Contributed by NM, 9-Jun-2006.)
⊢ (φ → ψ)    &   ⊢ (φ → (¬ χ → ¬ ψ))    ⇒   ⊢ (φ → χ)
Theorem	mt4i 131	Modus tollens inference. (Contributed by Wolf Lammen, 12-May-2013.)
⊢ χ    &   ⊢ (φ → (¬ ψ → ¬ χ))    ⇒   ⊢ (φ → ψ)
Theorem	nsyld 132	A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.)
⊢ (φ → (ψ → ¬ χ))    &   ⊢ (φ → (τ → χ))    ⇒   ⊢ (φ → (ψ → ¬ τ))
Theorem	nsyli 133	A negated syllogism inference. (Contributed by NM, 3-May-1994.)
⊢ (φ → (ψ → χ))    &   ⊢ (θ → ¬ χ)    ⇒   ⊢ (φ → (θ → ¬ ψ))
Theorem	nsyl4 134	A negated syllogism inference. (Contributed by NM, 15-Feb-1996.)
⊢ (φ → ψ)    &   ⊢ (¬ φ → χ)    ⇒   ⊢ (¬ χ → ψ)
Theorem	pm2.24d 135	Deduction version of pm2.24 101. (Contributed by NM, 30-Jan-2006.)
⊢ (φ → ψ)    ⇒   ⊢ (φ → (¬ ψ → χ))
Theorem	pm2.24i 136	Inference version of pm2.24 101. (Contributed by NM, 20-Aug-2001.)
⊢ φ    ⇒   ⊢ (¬ φ → ψ)
Theorem	pm3.2im 137	Theorem *3.2 of [WhiteheadRussell] p. 111, expressed with primitive connectives. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ (φ → (ψ → ¬ (φ → ¬ ψ)))
Theorem	mth8 138	Theorem 8 of [Margaris] p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ (φ → (¬ ψ → ¬ (φ → ψ)))
Theorem	jc 139	Inference joining the consequents of two premises. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ψ)    &   ⊢ (φ → χ)    ⇒   ⊢ (φ → ¬ (ψ → ¬ χ))
Theorem	impi 140	An importation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jul-2013.)
⊢ (φ → (ψ → χ))    ⇒   ⊢ (¬ (φ → ¬ ψ) → χ)
Theorem	expi 141	An exportation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.)
⊢ (¬ (φ → ¬ ψ) → χ)    ⇒   ⊢ (φ → (ψ → χ))
Theorem	simprim 142	Simplification. Similar to Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
⊢ (¬ (φ → ¬ ψ) → ψ)
Theorem	simplim 143	Simplification. Similar to Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Jul-2012.)
⊢ (¬ (φ → ψ) → φ)
Theorem	pm2.5 144	Theorem *2.5 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 9-Oct-2012.)
⊢ (¬ (φ → ψ) → (¬ φ → ψ))
Theorem	pm2.51 145	Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (φ → ψ) → (φ → ¬ ψ))
Theorem	pm2.521 146	Theorem *2.521 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.)
⊢ (¬ (φ → ψ) → (ψ → φ))
Theorem	pm2.52 147	Theorem *2.52 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.)
⊢ (¬ (φ → ψ) → (¬ φ → ¬ ψ))
Theorem	expt 148	Exportation theorem expressed with primitive connectives. (Contributed by NM, 5-Aug-1993.)
⊢ ((¬ (φ → ¬ ψ) → χ) → (φ → (ψ → χ)))
Theorem	impt 149	Importation theorem expressed with primitive connectives. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2013.)
⊢ ((φ → (ψ → χ)) → (¬ (φ → ¬ ψ) → χ))
Theorem	pm2.61d 150	Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (¬ ψ → χ))    ⇒   ⊢ (φ → χ)
Theorem	pm2.61d1 151	Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.)
⊢ (φ → (ψ → χ))    &   ⊢ (¬ ψ → χ)    ⇒   ⊢ (φ → χ)
Theorem	pm2.61d2 152	Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.)
⊢ (φ → (¬ ψ → χ))    &   ⊢ (ψ → χ)    ⇒   ⊢ (φ → χ)
Theorem	ja 153	Inference joining the antecedents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 19-Feb-2008.)
⊢ (¬ φ → χ)    &   ⊢ (ψ → χ)    ⇒   ⊢ ((φ → ψ) → χ)
Theorem	jad 154	Deduction form of ja 153. (Contributed by Scott Fenton, 13-Dec-2010.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)
⊢ (φ → (¬ ψ → θ))    &   ⊢ (φ → (χ → θ))    ⇒   ⊢ (φ → ((ψ → χ) → θ))
Theorem	jarl 155	Elimination of a nested antecedent as a kind of reversal of inference ja 153. (Contributed by Wolf Lammen, 10-May-2013.)
⊢ (((φ → ψ) → χ) → (¬ φ → χ))
Theorem	pm2.61i 156	Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)
⊢ (φ → ψ)    &   ⊢ (¬ φ → ψ)    ⇒   ⊢ ψ
Theorem	pm2.61ii 157	Inference eliminating two antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ (¬ φ → (¬ ψ → χ))    &   ⊢ (φ → χ)    &   ⊢ (ψ → χ)    ⇒   ⊢ χ
Theorem	pm2.61nii 158	Inference eliminating two antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
⊢ (φ → (ψ → χ))    &   ⊢ (¬ φ → χ)    &   ⊢ (¬ ψ → χ)    ⇒   ⊢ χ
Theorem	pm2.61iii 159	Inference eliminating three antecedents. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
⊢ (¬ φ → (¬ ψ → (¬ χ → θ)))    &   ⊢ (φ → θ)    &   ⊢ (ψ → θ)    &   ⊢ (χ → θ)    ⇒   ⊢ θ
Theorem	pm2.01 160	Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. (Contributed by NM, 18-Aug-1993.) (Proof shortened by O'Cat, 21-Nov-2008.) (Proof shortened by Wolf Lammen, 31-Oct-2012.)
⊢ ((φ → ¬ φ) → ¬ φ)
Theorem	pm2.01d 161	Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.)
⊢ (φ → (ψ → ¬ ψ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	pm2.6 162	Theorem *2.6 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ φ → ψ) → ((φ → ψ) → ψ))
Theorem	pm2.61 163	Theorem *2.61 of [WhiteheadRussell] p. 107. Useful for eliminating an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
⊢ ((φ → ψ) → ((¬ φ → ψ) → ψ))
Theorem	pm2.65 164	Theorem *2.65 of [WhiteheadRussell] p. 107. Proof by contradiction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Mar-2013.)
⊢ ((φ → ψ) → ((φ → ¬ ψ) → ¬ φ))
Theorem	pm2.65i 165	Inference rule for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
⊢ (φ → ψ)    &   ⊢ (φ → ¬ ψ)    ⇒   ⊢ ¬ φ
Theorem	pm2.65d 166	Deduction rule for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (ψ → ¬ χ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	mto 167	The rule of modus tollens. The rule says, "if ψ is not true, and φ implies ψ, then ψ must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mood that by denying affirms" [Sanford] p. 39. It is also called denying the consequent. Modus tollens is closely related to modus ponens ax-mp 5. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
⊢ ¬ ψ    &   ⊢ (φ → ψ)    ⇒   ⊢ ¬ φ
Theorem	mtod 168	Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
⊢ (φ → ¬ χ)    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	mtoi 169	Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
⊢ ¬ χ    &   ⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → ¬ ψ)
Theorem	mt2 170	A rule similar to modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.)
⊢ ψ    &   ⊢ (φ → ¬ ψ)    ⇒   ⊢ ¬ φ
Theorem	mt3 171	A rule similar to modus tollens. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
⊢ ¬ ψ    &   ⊢ (¬ φ → ψ)    ⇒   ⊢ φ
Theorem	peirce 172	Peirce's axiom. This odd-looking theorem is the "difference" between an intuitionistic system of propositional calculus and a classical system and is not accepted by intuitionists. When Peirce's axiom is added to an intuitionistic system, the system becomes equivalent to our classical system ax-1 6 through ax-3 8. A curious fact about this theorem is that it requires ax-3 8 for its proof even though the result has no negation connectives in it. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 9-Oct-2012.)
⊢ (((φ → ψ) → φ) → φ)
Theorem	loolin 173	The Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. For a version not using ax-3 8, see loolinALT 95. (Contributed by O'Cat, 12-Aug-2004.) (Proof shortened by Wolf Lammen, 2-Nov-2012.)
⊢ (((φ → ψ) → (ψ → φ)) → (ψ → φ))
Theorem	looinv 174	The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. Using dfor2 400, we can see that this essentially expresses "disjunction commutes." Theorem *2.69 of [WhiteheadRussell] p. 108. (Contributed by NM, 12-Aug-2004.)
⊢ (((φ → ψ) → ψ) → ((ψ → φ) → φ))
Theorem	bijust 175	Theorem used to justify definition of biconditional df-bi 177. (Contributed by NM, 11-May-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
⊢ ¬ ((¬ ((φ → ψ) → ¬ (ψ → φ)) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → ¬ ((φ → ψ) → ¬ (ψ → φ))))
1.2.5  Logical equivalence Definition df-bi 177 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 359 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.
Syntax	wb 176	Extend our wff definition to include the biconditional connective.
wff (φ ↔ ψ)
Definition	df-bi 177	Define the biconditional (logical 'iff'). Definition df-bi 177 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 359 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 936) 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 175. It is impossible to use df-bi 177 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 177 in the proof with the corresponding bijust 175 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 1319) and the constant false ⊥ (df-fal 1320), we will be able to prove these truth table values: (( ⊤ ↔ ⊤ ) ↔ ⊤ ) (trubitru 1350), (( ⊤ ↔ ⊥ ) ↔ ⊥ ) (trubifal 1351), (( ⊥ ↔ ⊤ ) ↔ ⊥ ) (falbitru 1352), and (( ⊥ ↔ ⊥ ) ↔ ⊤ ) (falbifal 1353). See dfbi1 184, dfbi2 609, and dfbi3 863 for theorems suggesting typical textbook definitions of ↔, showing that our definition has the properties we expect. Theorem dfbi1 184 is particularly useful if we want to eliminate ↔ from an expression to convert it to primitives. Theorem dfbi 610 shows this definition rewritten in an abbreviated form after conjunction is introduced, for easier understanding. Contrast with ∨ (df-or 359), → (wi 4), ⊼ (df-nan 1288), and ⊻ (df-xor 1305) . In some sense ↔ returns true if two truth values are equal; = (df-cleq 2346) returns true if two classes are equal. (Contributed by NM, 5-Aug-1993.)
⊢ ¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ)))
Theorem	bi1 178	Property of the biconditional connective. (Contributed by NM, 11-May-1999.)
⊢ ((φ ↔ ψ) → (φ → ψ))
Theorem	bi3 179	Property of the biconditional connective. (Contributed by NM, 11-May-1999.)
⊢ ((φ → ψ) → ((ψ → φ) → (φ ↔ ψ)))
Theorem	impbii 180	Infer an equivalence from an implication and its converse. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ψ)    &   ⊢ (ψ → φ)    ⇒   ⊢ (φ ↔ ψ)
Theorem	impbidd 181	Deduce an equivalence from two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (φ → (ψ → (χ → θ)))    &   ⊢ (φ → (ψ → (θ → χ)))    ⇒   ⊢ (φ → (ψ → (χ ↔ θ)))
Theorem	impbid21d 182	Deduce an equivalence from two implications. (Contributed by Wolf Lammen, 12-May-2013.)
⊢ (ψ → (χ → θ))    &   ⊢ (φ → (θ → χ))    ⇒   ⊢ (φ → (ψ → (χ ↔ θ)))
Theorem	impbid 183	Deduce an equivalence from two implications. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 3-Nov-2012.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (χ → ψ))    ⇒   ⊢ (φ → (ψ ↔ χ))
Theorem	dfbi1 184	Relate the biconditional connective to primitive connectives. See dfbi1gb 185 for an unusual version proved directly from axioms. (Contributed by NM, 5-Aug-1993.)
⊢ ((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ)))
Theorem	dfbi1gb 185	This proof of dfbi1 184, 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 177, compared to over 800 steps were the proof of dfbi1 184 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	biimpi 186	Infer an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (φ → ψ)
Theorem	sylbi 187	A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    &   ⊢ (ψ → χ)    ⇒   ⊢ (φ → χ)
Theorem	sylib 188	A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ψ)    &   ⊢ (ψ ↔ χ)    ⇒   ⊢ (φ → χ)
Theorem	bi2 189	Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
⊢ ((φ ↔ ψ) → (ψ → φ))
Theorem	bicom1 190	Commutative law for equivalence. (Contributed by Wolf Lammen, 10-Nov-2012.)
⊢ ((φ ↔ ψ) → (ψ ↔ φ))
Theorem	bicom 191	Commutative law for equivalence. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.)
⊢ ((φ ↔ ψ) ↔ (ψ ↔ φ))
Theorem	bicomd 192	Commute two sides of a biconditional in a deduction. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (χ ↔ ψ))
Theorem	bicomi 193	Inference from commutative law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (ψ ↔ φ)
Theorem	impbid1 194	Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.)
⊢ (φ → (ψ → χ))    &   ⊢ (χ → ψ)    ⇒   ⊢ (φ → (ψ ↔ χ))
Theorem	impbid2 195	Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.)
⊢ (ψ → χ)    &   ⊢ (φ → (χ → ψ))    ⇒   ⊢ (φ → (ψ ↔ χ))
Theorem	impcon4bid 196	A variation on impbid 183 with contraposition. (Contributed by Jeff Hankins, 3-Jul-2009.)
⊢ (φ → (ψ → χ))    &   ⊢ (φ → (¬ ψ → ¬ χ))    ⇒   ⊢ (φ → (ψ ↔ χ))
Theorem	biimpri 197	Infer a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Sep-2013.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (ψ → φ)
Theorem	biimpd 198	Deduce an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (ψ → χ))
Theorem	mpbi 199	An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
⊢ φ    &   ⊢ (φ ↔ ψ)    ⇒   ⊢ ψ
Theorem	mpbir 200	An inference from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)
⊢ ψ    &   ⊢ (φ ↔ ψ)    ⇒   ⊢ φ