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
Definition	df-an 401	Define conjunction (logical "and"). Definition of [Margaris] p. 49. When both the left and right operand are true, the result is true; when either is false, the result is false. For example, it is true that (2 = 2 ∧ 3 = 3). After we define the constant true ⊤ (df-tru 1566) and the constant false ⊥ (df-fal 1576), we will be able to prove these truth table values: ((⊤ ∧ ⊤) ↔ ⊤) (truantru 1596), ((⊤ ∧ ⊥) ↔ ⊥) (truanfal 1597), ((⊥ ∧ ⊤) ↔ ⊥) (falantru 1598), and ((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1599). This is our first use of the biconditional connective in a definition; we use the biconditional connective in place of the traditional "<=def=>", which means the same thing, except that we can manipulate the biconditional connective directly in proofs rather than having to rely on an informal definition substitution rule. Note that if we mechanically substitute ¬ (𝜑 → ¬ 𝜓) for (𝜑 ∧ 𝜓), we end up with an instance of previously proved theorem biid 264. This is the justification for the definition, along with the fact that it introduces a new symbol ∧. Contrast with ∨ (df-or 861), → (wi 4), ⊼ (df-nan 1515), and ⊻ (df-xor 1535). (Contributed by NM, 5-Jan-1993.)
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
Theorem	pm4.63 402	Theorem *4.63 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 → ¬ 𝜓) ↔ (𝜑 ∧ 𝜓))
Theorem	pm4.67 403	Theorem *4.67 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∧ 𝜓))
Theorem	imnan 404	Express an implication in terms of a negated conjunction. (Contributed by NM, 9-Apr-1994.)
⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
Theorem	imnani 405	Infer an implication from a negated conjunction. (Contributed by Mario Carneiro, 28-Sep-2015.)
⊢ ¬ (𝜑 ∧ 𝜓)    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	iman 406	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 407	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 408	Express a conjunction in terms of a negated implication. (Contributed by NM, 2-Aug-1994.)
⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))
Theorem	pm4.61 409	Theorem *4.61 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 → 𝜓) ↔ (𝜑 ∧ ¬ 𝜓))
Theorem	pm4.65 410	Theorem *4.65 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 → 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
Theorem	imp 411	Importation inference. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	impcom 412	Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
Theorem	con3dimp 413	Variant of con3d 153 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)
Theorem	mpnanrd 414	Eliminate the right side of a negated conjunction in an implication. (Contributed by ML, 17-Oct-2020.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → ¬ 𝜒)
Theorem	impd 415	Importation deduction. (Contributed by NM, 31-Mar-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	impcomd 416	Importation deduction with commuted antecedents. (Contributed by Peter Mazsa, 24-Sep-2022.) (Proof shortened by Wolf Lammen, 22-Oct-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
Theorem	ex 417	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 30663. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	expcom 418	Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → (𝜑 → 𝜒))
Theorem	expdcom 419	Commuted form of expd 420. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 420. (Revised by Wolf Lammen, 28-Jul-2022.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
Theorem	expd 420	Exportation deduction. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 28-Jul-2022.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	expcomd 421	Deduction form of expcom 418. (Contributed by Alan Sare, 22-Jul-2012.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
Theorem	imp31 422	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	imp32 423	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
Theorem	exp31 424	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	exp32 425	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	imp4b 426	An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 427. (Revised by Wolf Lammen, 19-Jul-2021.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
Theorem	imp4a 427	An importation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Jul-2021.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))
Theorem	imp4c 428	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏))
Theorem	imp4d 429	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏))
Theorem	imp41 430	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	imp42 431	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)
Theorem	imp43 432	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
Theorem	imp44 433	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏)
Theorem	imp45 434	An importation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜏)
Theorem	exp4b 435	An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 436. (Revised by Wolf Lammen, 20-Jul-2021.)
⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp4a 436	An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2021.)
⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp4c 437	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp4d 438	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (𝜑 → ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp41 439	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp42 440	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp43 441	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp44 442	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp45 443	An exportation inference. (Contributed by NM, 26-Apr-1994.)
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	imp5d 444	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂))
Theorem	imp5a 445	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) (Proof shortened by Wolf Lammen, 2-Aug-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → ((𝜃 ∧ 𝜏) → 𝜂))))
Theorem	imp5g 446	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (((𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂))
Theorem	imp55 447	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ (((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ∧ 𝜏) → 𝜂)
Theorem	imp511 448	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))    ⇒   ⊢ ((𝜑 ∧ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏)) → 𝜂)
Theorem	exp5c 449	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp5j 450	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → ((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp5l 451	An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp53 452	An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	pm3.3 453	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 454	Theorem *3.31 (Imp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒))
Theorem	impexp 455	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 456	Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))
Theorem	expdimp 457	A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
Theorem	expimpd 458	Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	impr 459	Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
Theorem	impl 460	Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	expr 461	Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
Theorem	expl 462	Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	ancoms 463	Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
Theorem	pm3.22 464	Theorem *3.22 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑))
Theorem	ancom 465	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 466	Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.)
⊢ (𝜑 → (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → (𝜒 ∧ 𝜓))
Theorem	biancomi 467	Commuting conjunction in a biconditional. (Contributed by Peter Mazsa, 17-Jun-2018.)
⊢ (𝜑 ↔ (𝜒 ∧ 𝜓))    ⇒   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
Theorem	biancomd 468	Commuting conjunction in a biconditional, deduction form. (Contributed by Peter Mazsa, 3-Oct-2018.)
⊢ (𝜑 → (𝜓 ↔ (𝜃 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
Theorem	ancomst 469	Closed form of ancoms 463. (Contributed by Alan Sare, 31-Dec-2011.)
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜓 ∧ 𝜑) → 𝜒))
Theorem	ancomsd 470	Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
Theorem	anasss 471	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
Theorem	anassrs 472	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	anass 473	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 474	Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. Its associated inference is pm3.2i 475 and its associated deduction is jca 520 (and the double deduction is jcad 521). See pm3.2im 161 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 475	Infer conjunction of premises. Inference associated with pm3.2 474. Its associated deduction is jca 520 (and the double deduction is jcad 521). (Contributed by NM, 21-Jun-1993.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ∧ 𝜓)
Theorem	pm3.21 476	Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
Theorem	pm3.43i 477	Nested conjunction of antecedents. (Contributed by NM, 4-Jan-1993.)
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜒) → (𝜑 → (𝜓 ∧ 𝜒))))
Theorem	pm3.43 478	Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∧ 𝜒)))
Theorem	dfbi2 479	A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 24-Jan-1993.)
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))
Theorem	dfbi 480	Definition df-bi 210 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 481	Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	biimpar 482	Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
Theorem	biimpac 483	Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
Theorem	biimparc 484	Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
Theorem	adantr 485	Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
Theorem	adantl 486	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 487	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 488	Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ 𝜑
Theorem	simpr 489	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 490	Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)
⊢ (𝜑 ∧ 𝜓)    ⇒   ⊢ 𝜓
Theorem	intnan 491	Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
⊢ ¬ 𝜑    ⇒   ⊢ ¬ (𝜓 ∧ 𝜑)
Theorem	intnanr 492	Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
⊢ ¬ 𝜑    ⇒   ⊢ ¬ (𝜑 ∧ 𝜓)
Theorem	intnand 493	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓))
Theorem	intnanrd 494	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
⊢ (𝜑 → ¬ 𝜓)    ⇒   ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))
Theorem	adantld 495	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 496	Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒))
Theorem	pm3.41 497	Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜒) → ((𝜑 ∧ 𝜓) → 𝜒))
Theorem	pm3.42 498	Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 → 𝜒) → ((𝜑 ∧ 𝜓) → 𝜒))
Theorem	simpld 499	Deduction eliminating a conjunct. A translation of natural deduction rule ∧ EL (∧ elimination left), see natded 30663. (Contributed by NM, 26-May-1993.)
⊢ (𝜑 → (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	simprd 500	Deduction eliminating a conjunct. (Contributed by NM, 14-May-1993.) A translation of natural deduction rule ∧ ER (∧ elimination right), see natded 30663. (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ (𝜑 → (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜑 → 𝜒)