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