P. 5 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 401-500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	imnani 401	Infer an implication from a negated conjunction. (Contributed by Mario Carneiro, 28-Sep-2015.)
⊢ ¬ (𝜑 ∧ 𝜓)    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	iman 402	Implication in terms of conjunction and negation. Theorem 3.4(27) of [Stoll] p. 176. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2012.)
⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓))
Theorem	pm3.24 403	Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who call it the "law of contradiction"). (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ¬ (𝜑 ∧ ¬ 𝜑)
Theorem	annim 404	Express a conjunction in terms of a negated implication. (Contributed by NM, 2-Aug-1994.)
⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))
Theorem	pm4.61 405	Theorem *4.61 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 → 𝜓) ↔ (𝜑 ∧ ¬ 𝜓))
Theorem	pm4.65 406	Theorem *4.65 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 → 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
Theorem	imp 407	Importation inference. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	impcom 408	Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
Theorem	con3dimp 409	Variant of con3d 152 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)
Theorem	mpnanrd 410	Eliminate the right side of a negated conjunction in an implication. (Contributed by ML, 17-Oct-2020.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	impd 411	Importation deduction. (Contributed by NM, 31-Mar-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	impcomd 412	Importation deduction with commuted antecedents. (Contributed by Peter Mazsa, 24-Sep-2022.) (Proof shortened by Wolf Lammen, 22-Oct-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
Theorem	ex 413	Exportation inference. (This theorem used to be labeled "exp" but was changed to "ex" so as not to conflict with the math token "exp", per the June 2006 Metamath spec change.) A translation of natural deduction rule → I (→ introduction), see natded 28776. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	expcom 414	Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → (𝜑 → 𝜒))
Theorem	expdcom 415	Commuted form of expd 416. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 416. (Revised by Wolf Lammen, 28-Jul-2022.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
Theorem	expd 416	Exportation deduction. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 28-Jul-2022.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	expcomd 417	Deduction form of expcom 414. (Contributed by Alan Sare, 22-Jul-2012.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
Theorem	imp31 418	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	imp32 419	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
Theorem	exp31 420	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	exp32 421	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	imp4b 422	An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 423. (Revised by Wolf Lammen, 19-Jul-2021.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
Theorem	imp4a 423	An importation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Jul-2021.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))
Theorem	imp4c 424	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏))
Theorem	imp4d 425	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏))
Theorem	imp41 426	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	imp42 427	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)
Theorem	imp43 428	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
Theorem	imp44 429	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏)
Theorem	imp45 430	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜏)
Theorem	exp4b 431	An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 432. (Revised by Wolf Lammen, 20-Jul-2021.)
⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp4a 432	An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2021.)
⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp4c 433	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp4d 434	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp41 435	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp42 436	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp43 437	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp44 438	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp45 439	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	imp5d 440	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂))
Theorem	imp5a 441	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) (Proof shortened by Wolf Lammen, 2-Aug-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → ((𝜃 ∧ 𝜏) → 𝜂))))
Theorem	imp5g 442	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (((𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂))
Theorem	imp55 443	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ∧ 𝜏) → 𝜂)
Theorem	imp511 444	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ ((𝜑 ∧ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏)) → 𝜂)
Theorem	exp5c 445	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp5j 446	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → ((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp5l 447	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp53 448	An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	pm3.3 449	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 450	Theorem *3.31 (Imp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒))
Theorem	impexp 451	Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))
Theorem	impancom 452	Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))
Theorem	expdimp 453	A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
Theorem	expimpd 454	Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	impr 455	Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
Theorem	impl 456	Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	expr 457	Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
Theorem	expl 458	Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	ancoms 459	Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
Theorem	pm3.22 460	Theorem *3.22 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))
Theorem	ancom 461	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 462	Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.)
⊢ (𝜑 → (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ∧ 𝜓))
Theorem	biancomi 463	Commuting conjunction in a biconditional. (Contributed by Peter Mazsa, 17-Jun-2018.)
⊢ (𝜑 ↔ (𝜒 ∧ 𝜓))    ⇒   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
Theorem	biancomd 464	Commuting conjunction in a biconditional, deduction form. (Contributed by Peter Mazsa, 3-Oct-2018.)
⊢ (𝜑 → (𝜓 ↔ (𝜃 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
Theorem	ancomst 465	Closed form of ancoms 459. (Contributed by Alan Sare, 31-Dec-2011.)
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜓 ∧ 𝜑) → 𝜒))
Theorem	ancomsd 466	Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
Theorem	anasss 467	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
Theorem	anassrs 468	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	anass 469	Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
Theorem	pm3.2 470	Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. Its associated inference is pm3.2i 471 and its associated deduction is jca 512 (and the double deduction is jcad 513). See pm3.2im 160 for a version using only implication and negation. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
Theorem	pm3.2i 471	Infer conjunction of premises. Inference associated with pm3.2 470. Its associated deduction is jca 512 (and the double deduction is jcad 513). (Contributed by NM, 21-Jun-1993.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ∧ 𝜓)
Theorem	pm3.21 472	Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
Theorem	pm3.43i 473	Nested conjunction of antecedents. (Contributed by NM, 4-Jan-1993.)
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜒) → (𝜑 → (𝜓 ∧ 𝜒))))
Theorem	pm3.43 474	Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∧ 𝜒)))
Theorem	dfbi2 475	A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 24-Jan-1993.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))
Theorem	dfbi 476	Definition df-bi 206 rewritten in an abbreviated form to help intuitive understanding of that definition. Note that it is a conjunction of two implications; one which asserts properties that follow from the biconditional and one which asserts properties that imply the biconditional. (Contributed by NM, 15-Aug-2008.)
⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
Theorem	biimpa 477	Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	biimpar 478	Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
Theorem	biimpac 479	Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
Theorem	biimparc 480	Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
Theorem	adantr 481	Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
Theorem	adantl 482	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	simpl 483	Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜑)
Theorem	simpli 484	Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ 𝜑
Theorem	simpr 485	Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜓)
Theorem	simpri 486	Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ 𝜓
Theorem	intnan 487	Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
⊢ ¬ 𝜑    ⇒   ⊢ ¬ (𝜓 ∧ 𝜑)
Theorem	intnanr 488	Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
⊢ ¬ 𝜑    ⇒   ⊢ ¬ (𝜑 ∧ 𝜓)
Theorem	intnand 489	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))
Theorem	intnanrd 490	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))
Theorem	adantld 491	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 492	Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))
Theorem	pm3.41 493	Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜒) → ((𝜑 ∧ 𝜓) → 𝜒))
Theorem	pm3.42 494	Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 → 𝜒) → ((𝜑 ∧ 𝜓) → 𝜒))
Theorem	simpld 495	Deduction eliminating a conjunct. A translation of natural deduction rule ∧ EL (∧ elimination left), see natded 28776. (Contributed by NM, 26-May-1993.)
⊢ (𝜑 → (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	simprd 496	Deduction eliminating a conjunct. (Contributed by NM, 14-May-1993.) A translation of natural deduction rule ∧ ER (∧ elimination right), see natded 28776. (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ (𝜑 → (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simprbi 497	Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simplbi 498	Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	simprbda 499	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	simplbda 500	Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)