P. 9 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 801-900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	adantl3r 801	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ((((𝜑 ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)    ⇒   ⊢ (((((𝜑 ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)
Theorem	adantl4r 802	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ (((((𝜑 ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)    ⇒   ⊢ ((((((𝜑 ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)
Theorem	adantl5r 803	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ((((((𝜑 ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)    ⇒   ⊢ (((((((𝜑 ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)
Theorem	adantl6r 804	Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ (((((((𝜑 ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)    ⇒   ⊢ ((((((((𝜑 ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅)
Theorem	simpll 805	Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
Theorem	simplld 806	Deduction form of simpll 805, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	simplr 807	Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
Theorem	simplrd 808	Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simprl 809	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜓)
Theorem	simprld 810	Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simprr 811	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜒)
Theorem	simprrd 812	Deduction form of simprr 811, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	simplll 813	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) (Proof shortened by Wolf Lammen, 6-Apr-2022.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)
Theorem	simplllOLD 814	Obsolete version of simplll 813 as of 6-Apr-2022. (Contributed by Jeff Hankins, 28-Jul-2009.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)
Theorem	simpllr 815	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) (Proof shortened by Wolf Lammen, 6-Apr-2022.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
Theorem	simpllrOLD 816	Obsolete version of simpllr 815 as of 6-Apr-2022. (Contributed by Jeff Hankins, 28-Jul-2009.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓)
Theorem	simplrl 817	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)
Theorem	simplrr 818	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)
Theorem	simprll 819	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓)
Theorem	simprlr 820	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)
Theorem	simprrl 821	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒)
Theorem	simprrr 822	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)
Theorem	simp-4l 823	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Theorem	simp-4r 824	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Theorem	simp-5l 825	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑)
Theorem	simp-5r 826	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
Theorem	simp-6l 827	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑)
Theorem	simp-6r 828	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
Theorem	simp-7l 829	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜑)
Theorem	simp-7r 830	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓)
Theorem	simp-8l 831	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜑)
Theorem	simp-8r 832	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓)
Theorem	simp-9l 833	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜑)
Theorem	simp-9r 834	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓)
Theorem	simp-10l 835	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜑)
Theorem	simp-10r 836	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜓)
Theorem	simp-11l 837	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜑)
Theorem	simp-11r 838	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜓)
Theorem	jaob 839	Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓)))
Theorem	adant423OLD 840	Obsolete as of 2-Oct-2021. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒)
Theorem	jaoian 841	Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒)
Theorem	jao1i 842	Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.)
⊢ (𝜓 → (𝜒 → 𝜑))    ⇒   ⊢ ((𝜑 ∨ 𝜓) → (𝜒 → 𝜑))
Theorem	jaodan 843	Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
Theorem	mpjaodan 844	Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 27390. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm4.77 845	Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) ↔ ((𝜓 ∨ 𝜒) → 𝜑))
Theorem	pm2.63 846	Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜑 ∨ 𝜓) → 𝜓))
Theorem	pm2.64 847	Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ ¬ 𝜓) → 𝜑))
Theorem	pm2.61ian 848	Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (𝜓 → 𝜒)
Theorem	pm2.61dan 849	Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm2.61ddan 850	Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.)
⊢ ((𝜑 ∧ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ ¬ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	pm2.61dda 851	Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.)
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜃)    &   ⊢ ((𝜑 ∧ ¬ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	condan 852	Proof by contradiction. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Wolf Lammen, 19-Jun-2014.)
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ 𝜒)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	abai 853	Introduce one conjunct as an antecedent to the other. "abai" stands for "and, biconditional, and, implication". (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (𝜑 → 𝜓)))
Theorem	pm5.53 854	Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((((𝜑 ∨ 𝜓) ∨ 𝜒) → 𝜃) ↔ (((𝜑 → 𝜃) ∧ (𝜓 → 𝜃)) ∧ (𝜒 → 𝜃)))
Theorem	an12 855	Swap two conjuncts. Note that the first digit (1) in the label refers to the outer conjunct position, and the next digit (2) to the inner conjunct position. (Contributed by NM, 12-Mar-1995.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
Theorem	an32 856	A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	an13 857	A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜑)))
Theorem	an31 858	A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑))
Theorem	bianass 859	An inference to merge two lists of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ ((𝜂 ∧ 𝜑) ↔ ((𝜂 ∧ 𝜓) ∧ 𝜒))
Theorem	an12s 860	Swap two conjuncts in antecedent. The label suffix "s" means that an12 855 is combined with syl 17 (or a variant). (Contributed by NM, 13-Mar-1996.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃)
Theorem	ancom2s 861	Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)
Theorem	an13s 862	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑)) → 𝜃)
Theorem	an32s 863	Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)
Theorem	ancom1s 864	Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃)
Theorem	an31s 865	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜒 ∧ 𝜓) ∧ 𝜑) → 𝜃)
Theorem	anass1rs 866	Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃)
Theorem	anabs1 867	Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) ↔ (𝜑 ∧ 𝜓))
Theorem	anabs5 868	Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓))
Theorem	anabs7 869	Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 17-Nov-2013.)
⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓))
Theorem	a2and 870	Deduction distributing a conjunction as embedded antecedent. (Contributed by AV, 25-Oct-2019.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)
⊢ (𝜑 → ((𝜓 ∧ 𝜌) → (𝜏 → 𝜃)))    &   ⊢ (𝜑 → ((𝜓 ∧ 𝜌) → 𝜒))    ⇒   ⊢ (𝜑 → (((𝜓 ∧ 𝜒) → 𝜏) → ((𝜓 ∧ 𝜌) → 𝜃)))
Theorem	anabsan 871	Absorption of antecedent with conjunction. (Contributed by NM, 24-Mar-1996.)
⊢ (((𝜑 ∧ 𝜑) ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabss1 872	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabss4 873	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.)
⊢ (((𝜓 ∧ 𝜑) ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabss5 874	Absorption of antecedent into conjunction. (Contributed by NM, 10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabsi5 875	Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabsi6 876	Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.)
⊢ (𝜑 → ((𝜓 ∧ 𝜑) → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabsi7 877	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
⊢ (𝜓 → ((𝜑 ∧ 𝜓) → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabsi8 878	Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.)
⊢ (𝜓 → ((𝜓 ∧ 𝜑) → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabss7 879	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 19-Nov-2013.)
⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabsan2 880	Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	anabss3 881	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	an4 882	Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)))
Theorem	an42 883	Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)))
Theorem	an43 884	Rearrangement of 4 conjuncts. (Contributed by Rodolfo Medina, 24-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜒)))
Theorem	an3 885	A rearrangement of conjuncts. (Contributed by Rodolfo Medina, 25-Sep-2010.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → (𝜑 ∧ 𝜃))
Theorem	an4s 886	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)
Theorem	an42s 887	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏)
Theorem	anandi 888	Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
Theorem	anandir 889	Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒)))
Theorem	anandis 890	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)
Theorem	anandirs 891	Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒)) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜏)
Theorem	syl2an2 892	syl2an 493 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜒 ∧ 𝜑) → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜒 ∧ 𝜑) → 𝜏)
Theorem	syl2an2r 893	syl2anr 494 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Mar-2022.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜏)
Theorem	syl2an2rOLD 894	Obsolete proof of syl2an2r 893 as of 28-Mar-2022. (Contributed by Alan Sare, 27-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜏)
Theorem	impbida 895	Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜒))
Theorem	pm3.48 896	Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)))
Theorem	pm3.45 897	Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) → ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒)))
Theorem	im2anan9 898	Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂)))
Theorem	im2anan9r 899	Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂)))
Theorem	anim12dan 900	Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏))