P. 3 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 201-300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3imtr4i 201	A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    ⇒   ⊢ (𝜒 → 𝜃)
Theorem	3imtr3d 202	More general version of 3imtr3i 200. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜃 → 𝜏))
Theorem	3imtr4d 203	More general version of 3imtr4i 201. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜓))    &   ⊢ (𝜑 → (𝜏 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜃 → 𝜏))
Theorem	3imtr3g 204	More general version of 3imtr3i 200. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜓 ↔ 𝜃)    &   ⊢ (𝜒 ↔ 𝜏)    ⇒   ⊢ (𝜑 → (𝜃 → 𝜏))
Theorem	3imtr4g 205	More general version of 3imtr4i 201. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜒)    ⇒   ⊢ (𝜑 → (𝜃 → 𝜏))
Theorem	3bitri 206	A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜑 ↔ 𝜃)
Theorem	3bitrri 207	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ 𝜒)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜃 ↔ 𝜑)
Theorem	3bitr2i 208	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜑 ↔ 𝜃)
Theorem	3bitr2ri 209	A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (𝜃 ↔ 𝜑)
Theorem	3bitr3i 210	A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜑 ↔ 𝜒)    &   ⊢ (𝜓 ↔ 𝜃)    ⇒   ⊢ (𝜒 ↔ 𝜃)
Theorem	3bitr3ri 211	A chained inference from transitive law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜑 ↔ 𝜒)    &   ⊢ (𝜓 ↔ 𝜃)    ⇒   ⊢ (𝜃 ↔ 𝜒)
Theorem	3bitr4i 212	A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    ⇒   ⊢ (𝜒 ↔ 𝜃)
Theorem	3bitr4ri 213	A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜓)    ⇒   ⊢ (𝜃 ↔ 𝜒)
Theorem	3bitrd 214	Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜏))
Theorem	3bitrrd 215	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜃))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜏 ↔ 𝜓))
Theorem	3bitr2d 216	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜏))
Theorem	3bitr2rd 217	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜏 ↔ 𝜓))
Theorem	3bitr3d 218	Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜏))
Theorem	3bitr3rd 219	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → (𝜒 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜏 ↔ 𝜃))
Theorem	3bitr4d 220	Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜓))    &   ⊢ (𝜑 → (𝜏 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜏))
Theorem	3bitr4rd 221	Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜓))    &   ⊢ (𝜑 → (𝜏 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝜏 ↔ 𝜃))
Theorem	3bitr3g 222	More general version of 3bitr3i 210. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜓 ↔ 𝜃)    &   ⊢ (𝜒 ↔ 𝜏)    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜏))
Theorem	3bitr4g 223	More general version of 3bitr4i 212. Useful for converting definitions in a formula. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜃 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜒)    ⇒   ⊢ (𝜑 → (𝜃 ↔ 𝜏))
Theorem	bi3ant 224	Construct a biconditional in antecedent position. (Contributed by Wolf Lammen, 14-May-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (((𝜃 → 𝜏) → 𝜑) → (((𝜏 → 𝜃) → 𝜓) → ((𝜃 ↔ 𝜏) → 𝜒)))
Theorem	bisym 225	Express symmetries of theorems in terms of biconditionals. (Contributed by Wolf Lammen, 14-May-2013.)
⊢ (((𝜑 → 𝜓) → (𝜒 → 𝜃)) → (((𝜓 → 𝜑) → (𝜃 → 𝜒)) → ((𝜑 ↔ 𝜓) → (𝜒 ↔ 𝜃))))
Theorem	imbi2i 226	Introduce an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))
Theorem	bibi2i 227	Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))
Theorem	bibi1i 228	Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))
Theorem	bibi12i 229	The equivalence of two equivalences. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜃))
Theorem	imbi2d 230	Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒)))
Theorem	imbi1d 231	Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))
Theorem	bibi2d 232	Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))
Theorem	bibi1d 233	Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))
Theorem	imbi12d 234	Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏)))
Theorem	bibi12d 235	Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏)))
Theorem	imbi1 236	Theorem *4.84 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
Theorem	imbi2 237	Theorem *4.85 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)))
Theorem	imbi1i 238	Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))
Theorem	imbi12i 239	Join two logical equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃))
Theorem	bibi1 240	Theorem *4.86 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)))
Theorem	biimt 241	A wff is equivalent to itself with true antecedent. (Contributed by NM, 28-Jan-1996.)
⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))
Theorem	pm5.5 242	Theorem *5.5 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓))
Theorem	a1bi 243	Inference introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜑 → 𝜓))
Theorem	pm5.501 244	Theorem *5.501 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 24-Jan-2013.)
⊢ (𝜑 → (𝜓 ↔ (𝜑 ↔ 𝜓)))
Theorem	ibib 245	Implication in terms of implication and biconditional. (Contributed by NM, 31-Mar-1994.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜑 ↔ 𝜓)))
Theorem	ibibr 246	Implication in terms of implication and biconditional. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 21-Dec-2013.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜓 ↔ 𝜑)))
Theorem	tbt 247	A wff is equivalent to its equivalence with truth. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜓 ↔ 𝜑))
Theorem	bi2.04 248	Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))
Theorem	pm5.4 249	Antecedent absorption implication. Theorem *5.4 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.)
⊢ ((𝜑 → (𝜑 → 𝜓)) ↔ (𝜑 → 𝜓))
Theorem	imdi 250	Distributive law for implication. Compare Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	pm5.41 251	Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 12-Oct-2012.)
⊢ (((𝜑 → 𝜓) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 → 𝜒)))
Theorem	imbibi 252	The antecedent of one side of a biconditional can be moved out of the biconditional to become the antecedent of the remaining biconditional. (Contributed by BJ, 1-Jan-2025.) (Proof shortened by Wolf Lammen, 5-Jan-2025.)
⊢ (((𝜑 → 𝜓) ↔ 𝜒) → (𝜑 → (𝜓 ↔ 𝜒)))
Theorem	imim21b 253	Simplify an implication between two implications when the antecedent of the first is a consequence of the antecedent of the second. The reverse form is useful in producing the successor step in induction proofs. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Wolf Lammen, 14-Sep-2013.)
⊢ ((𝜓 → 𝜑) → (((𝜑 → 𝜒) → (𝜓 → 𝜃)) ↔ (𝜓 → (𝜒 → 𝜃))))
Theorem	impd 254	Importation deduction. (Contributed by NM, 31-Mar-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	impcomd 255	Importation deduction with commuted antecedents. (Contributed by Peter Mazsa, 24-Sep-2022.) (Proof shortened by Wolf Lammen, 22-Oct-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
Theorem	imp31 256	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	imp32 257	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
Theorem	expd 258	Exportation deduction. (Contributed by NM, 20-Aug-1993.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	expdimp 259	A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
Theorem	impancom 260	Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))
Theorem	pm3.3 261	Theorem *3.3 (Exp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒)))
Theorem	pm3.31 262	Theorem *3.31 (Imp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒))
Theorem	impexp 263	Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))
Theorem	pm3.21 264	Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
Theorem	pm3.22 265	Theorem *3.22 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))
Theorem	ancom 266	Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
Theorem	ancomd 267	Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.)
⊢ (𝜑 → (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ∧ 𝜓))
Theorem	ancoms 268	Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
Theorem	ancomsd 269	Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
Theorem	biancomi 270	Commuting conjunction in a biconditional. (Contributed by Peter Mazsa, 17-Jun-2018.)
⊢ (𝜑 ↔ (𝜒 ∧ 𝜓))    ⇒   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
Theorem	biancomd 271	Commuting conjunction in a biconditional, deduction form. (Contributed by Peter Mazsa, 3-Oct-2018.)
⊢ (𝜑 → (𝜓 ↔ (𝜃 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
Theorem	pm3.2i 272	Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ∧ 𝜓)
Theorem	pm3.43i 273	Nested conjunction of antecedents. (Contributed by NM, 5-Aug-1993.)
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜒) → (𝜑 → (𝜓 ∧ 𝜒))))
Theorem	simplbi 274	Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	simprbi 275	Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	adantr 276	Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
Theorem	adantl 277	Inference adding a conjunct to the left of an antecedent. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
Theorem	adantld 278	Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜒))
Theorem	adantrd 279	Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))
Theorem	impel 280	An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
Theorem	mpan9 281	Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → (𝜓 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	syldan 282	A syllogism deduction with conjoined antecents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	sylan 283	A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	sylanb 284	A syllogism inference. (Contributed by NM, 18-May-1994.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	sylanbr 285	A syllogism inference. (Contributed by NM, 18-May-1994.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
Theorem	sylan2 286	A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜃)
Theorem	sylan2b 287	A syllogism inference. (Contributed by NM, 21-Apr-1994.)
⊢ (𝜑 ↔ 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜃)
Theorem	sylan2br 288	A syllogism inference. (Contributed by NM, 21-Apr-1994.)
⊢ (𝜒 ↔ 𝜑)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜃)
Theorem	syl2an 289	A double syllogism inference. (Contributed by NM, 31-Jan-1997.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜏 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
Theorem	syl2anr 290	A double syllogism inference. (Contributed by NM, 17-Sep-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜏 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜏 ∧ 𝜑) → 𝜃)
Theorem	syl2anb 291	A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜏 ↔ 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
Theorem	syl2anbr 292	A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (𝜒 ↔ 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
Theorem	syland 293	A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏))
Theorem	sylan2d 294	A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜏))
Theorem	syl2and 295	A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂))
Theorem	biimpa 296	Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	biimpar 297	Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
Theorem	biimpac 298	Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
Theorem	biimparc 299	Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
Theorem	iba 300	Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.) (Revised by NM, 24-Mar-2013.)
⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))