P. 8 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 701-800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	adantlrr 701	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ (((φ ∧ (ψ ∧ τ)) ∧ χ) → θ)
Theorem	adantrll 702	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ ((τ ∧ ψ) ∧ χ)) → θ)
Theorem	adantrlr 703	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ ((ψ ∧ τ) ∧ χ)) → θ)
Theorem	adantrrl 704	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ (ψ ∧ (τ ∧ χ))) → θ)
Theorem	adantrrr 705	Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ (ψ ∧ (χ ∧ τ))) → θ)
Theorem	ad2antrr 706	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
⊢ (φ → ψ)    ⇒   ⊢ (((φ ∧ χ) ∧ θ) → ψ)
Theorem	ad2antlr 707	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
⊢ (φ → ψ)    ⇒   ⊢ (((χ ∧ φ) ∧ θ) → ψ)
Theorem	ad2antrl 708	Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
⊢ (φ → ψ)    ⇒   ⊢ ((χ ∧ (φ ∧ θ)) → ψ)
Theorem	ad2antll 709	Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)
⊢ (φ → ψ)    ⇒   ⊢ ((χ ∧ (θ ∧ φ)) → ψ)
Theorem	ad3antrrr 710	Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
⊢ (φ → ψ)    ⇒   ⊢ ((((φ ∧ χ) ∧ θ) ∧ τ) → ψ)
Theorem	ad3antlr 711	Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ ((((χ ∧ φ) ∧ θ) ∧ τ) → ψ)
Theorem	ad4antr 712	Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ (((((φ ∧ χ) ∧ θ) ∧ τ) ∧ η) → ψ)
Theorem	ad4antlr 713	Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ (((((χ ∧ φ) ∧ θ) ∧ τ) ∧ η) → ψ)
Theorem	ad5antr 714	Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ ((((((φ ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) → ψ)
Theorem	ad5antlr 715	Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ ((((((χ ∧ φ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) → ψ)
Theorem	ad6antr 716	Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ (((((((φ ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) → ψ)
Theorem	ad6antlr 717	Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ (((((((χ ∧ φ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) → ψ)
Theorem	ad7antr 718	Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ ((((((((φ ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) → ψ)
Theorem	ad7antlr 719	Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ ((((((((χ ∧ φ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) → ψ)
Theorem	ad8antr 720	Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ (((((((((φ ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) ∧ μ) → ψ)
Theorem	ad8antlr 721	Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ (((((((((χ ∧ φ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) ∧ μ) → ψ)
Theorem	ad9antr 722	Deduction adding 9 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ ((((((((((φ ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) ∧ μ) ∧ λ) → ψ)
Theorem	ad9antlr 723	Deduction adding 9 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ ((((((((((χ ∧ φ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) ∧ μ) ∧ λ) → ψ)
Theorem	ad10antr 724	Deduction adding 10 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ (((((((((((φ ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) ∧ μ) ∧ λ) ∧ κ) → ψ)
Theorem	ad10antlr 725	Deduction adding 10 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.)
⊢ (φ → ψ)    ⇒   ⊢ (((((((((((χ ∧ φ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) ∧ μ) ∧ λ) ∧ κ) → ψ)
Theorem	ad2ant2l 726	Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (((θ ∧ φ) ∧ (τ ∧ ψ)) → χ)
Theorem	ad2ant2r 727	Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (((φ ∧ θ) ∧ (ψ ∧ τ)) → χ)
Theorem	ad2ant2lr 728	Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (((θ ∧ φ) ∧ (ψ ∧ τ)) → χ)
Theorem	ad2ant2rl 729	Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)
⊢ ((φ ∧ ψ) → χ)    ⇒   ⊢ (((φ ∧ θ) ∧ (τ ∧ ψ)) → χ)
Theorem	simpll 730	Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.)
⊢ (((φ ∧ ψ) ∧ χ) → φ)
Theorem	simplr 731	Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.)
⊢ (((φ ∧ ψ) ∧ χ) → ψ)
Theorem	simprl 732	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
⊢ ((φ ∧ (ψ ∧ χ)) → ψ)
Theorem	simprr 733	Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.)
⊢ ((φ ∧ (ψ ∧ χ)) → χ)
Theorem	simplll 734	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((((φ ∧ ψ) ∧ χ) ∧ θ) → φ)
Theorem	simpllr 735	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((((φ ∧ ψ) ∧ χ) ∧ θ) → ψ)
Theorem	simplrl 736	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ (((φ ∧ (ψ ∧ χ)) ∧ θ) → ψ)
Theorem	simplrr 737	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ (((φ ∧ (ψ ∧ χ)) ∧ θ) → χ)
Theorem	simprll 738	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((φ ∧ ((ψ ∧ χ) ∧ θ)) → ψ)
Theorem	simprlr 739	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((φ ∧ ((ψ ∧ χ) ∧ θ)) → χ)
Theorem	simprrl 740	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((φ ∧ (ψ ∧ (χ ∧ θ))) → χ)
Theorem	simprrr 741	Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
⊢ ((φ ∧ (ψ ∧ (χ ∧ θ))) → θ)
Theorem	simp-4l 742	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) → φ)
Theorem	simp-4r 743	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) → ψ)
Theorem	simp-5l 744	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) → φ)
Theorem	simp-5r 745	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) → ψ)
Theorem	simp-6l 746	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) → φ)
Theorem	simp-6r 747	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) → ψ)
Theorem	simp-7l 748	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) → φ)
Theorem	simp-7r 749	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) → ψ)
Theorem	simp-8l 750	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) → φ)
Theorem	simp-8r 751	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) → ψ)
Theorem	simp-9l 752	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) ∧ μ) → φ)
Theorem	simp-9r 753	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) ∧ μ) → ψ)
Theorem	simp-10l 754	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) ∧ μ) ∧ λ) → φ)
Theorem	simp-10r 755	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ (((((((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) ∧ μ) ∧ λ) → ψ)
Theorem	simp-11l 756	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) ∧ μ) ∧ λ) ∧ κ) → φ)
Theorem	simp-11r 757	Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((((((((((((φ ∧ ψ) ∧ χ) ∧ θ) ∧ τ) ∧ η) ∧ ζ) ∧ σ) ∧ ρ) ∧ μ) ∧ λ) ∧ κ) → ψ)
Theorem	jaob 758	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	jaoian 759	Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.)
⊢ ((φ ∧ ψ) → χ)    &   ⊢ ((θ ∧ ψ) → χ)    ⇒   ⊢ (((φ ∨ θ) ∧ ψ) → χ)
Theorem	jaodan 760	Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)
⊢ ((φ ∧ ψ) → χ)    &   ⊢ ((φ ∧ θ) → χ)    ⇒   ⊢ ((φ ∧ (ψ ∨ θ)) → χ)
Theorem	mpjaodan 761	Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E ( ∨ elimination), see natded in set.mm. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ ((φ ∧ ψ) → χ)    &   ⊢ ((φ ∧ θ) → χ)    &   ⊢ (φ → (ψ ∨ θ))    ⇒   ⊢ (φ → χ)
Theorem	pm4.77 762	Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
⊢ (((ψ → φ) ∧ (χ → φ)) ↔ ((ψ ∨ χ) → φ))
Theorem	pm2.63 763	Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ ∨ ψ) → ((¬ φ ∨ ψ) → ψ))
Theorem	pm2.64 764	Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((φ ∨ ψ) → ((φ ∨ ¬ ψ) → φ))
Theorem	pm2.61ian 765	Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
⊢ ((φ ∧ ψ) → χ)    &   ⊢ ((¬ φ ∧ ψ) → χ)    ⇒   ⊢ (ψ → χ)
Theorem	pm2.61dan 766	Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
⊢ ((φ ∧ ψ) → χ)    &   ⊢ ((φ ∧ ¬ ψ) → χ)    ⇒   ⊢ (φ → χ)
Theorem	pm2.61ddan 767	Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.)
⊢ ((φ ∧ ψ) → θ)    &   ⊢ ((φ ∧ χ) → θ)    &   ⊢ ((φ ∧ (¬ ψ ∧ ¬ χ)) → θ)    ⇒   ⊢ (φ → θ)
Theorem	pm2.61dda 768	Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.)
⊢ ((φ ∧ ¬ ψ) → θ)    &   ⊢ ((φ ∧ ¬ χ) → θ)    &   ⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ (φ → θ)
Theorem	condan 769	Proof by contradiction. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Wolf Lammen, 19-Jun-2014.)
⊢ ((φ ∧ ¬ ψ) → χ)    &   ⊢ ((φ ∧ ¬ ψ) → ¬ χ)    ⇒   ⊢ (φ → ψ)
Theorem	abai 770	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 771	Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((((φ ∨ ψ) ∨ χ) → θ) ↔ (((φ → θ) ∧ (ψ → θ)) ∧ (χ → θ)))
Theorem	an12 772	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 773	A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
⊢ (((φ ∧ ψ) ∧ χ) ↔ ((φ ∧ χ) ∧ ψ))
Theorem	an13 774	A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
⊢ ((φ ∧ (ψ ∧ χ)) ↔ (χ ∧ (ψ ∧ φ)))
Theorem	an31 775	A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
⊢ (((φ ∧ ψ) ∧ χ) ↔ ((χ ∧ ψ) ∧ φ))
Theorem	an12s 776	Swap two conjuncts in antecedent. The label suffix "s" means that an12 772 is combined with syl 15 (or a variant). (Contributed by NM, 13-Mar-1996.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((ψ ∧ (φ ∧ χ)) → θ)
Theorem	ancom2s 777	Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((φ ∧ (χ ∧ ψ)) → θ)
Theorem	an13s 778	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ ((χ ∧ (ψ ∧ φ)) → θ)
Theorem	an32s 779	Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ (((φ ∧ χ) ∧ ψ) → θ)
Theorem	ancom1s 780	Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ (((ψ ∧ φ) ∧ χ) → θ)
Theorem	an31s 781	Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
⊢ (((φ ∧ ψ) ∧ χ) → θ)    ⇒   ⊢ (((χ ∧ ψ) ∧ φ) → θ)
Theorem	anass1rs 782	Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.)
⊢ ((φ ∧ (ψ ∧ χ)) → θ)    ⇒   ⊢ (((φ ∧ χ) ∧ ψ) → θ)
Theorem	anabs1 783	Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
⊢ (((φ ∧ ψ) ∧ φ) ↔ (φ ∧ ψ))
Theorem	anabs5 784	Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
⊢ ((φ ∧ (φ ∧ ψ)) ↔ (φ ∧ ψ))
Theorem	anabs7 785	Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 17-Nov-2013.)
⊢ ((ψ ∧ (φ ∧ ψ)) ↔ (φ ∧ ψ))
Theorem	anabsan 786	Absorption of antecedent with conjunction. (Contributed by NM, 24-Mar-1996.)
⊢ (((φ ∧ φ) ∧ ψ) → χ)    ⇒   ⊢ ((φ ∧ ψ) → χ)
Theorem	anabss1 787	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
⊢ (((φ ∧ ψ) ∧ φ) → χ)    ⇒   ⊢ ((φ ∧ ψ) → χ)
Theorem	anabss4 788	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.)
⊢ (((ψ ∧ φ) ∧ ψ) → χ)    ⇒   ⊢ ((φ ∧ ψ) → χ)
Theorem	anabss5 789	Absorption of antecedent into conjunction. (Contributed by NM, 10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
⊢ ((φ ∧ (φ ∧ ψ)) → χ)    ⇒   ⊢ ((φ ∧ ψ) → χ)
Theorem	anabsi5 790	Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
⊢ (φ → ((φ ∧ ψ) → χ))    ⇒   ⊢ ((φ ∧ ψ) → χ)
Theorem	anabsi6 791	Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.)
⊢ (φ → ((ψ ∧ φ) → χ))    ⇒   ⊢ ((φ ∧ ψ) → χ)
Theorem	anabsi7 792	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
⊢ (ψ → ((φ ∧ ψ) → χ))    ⇒   ⊢ ((φ ∧ ψ) → χ)
Theorem	anabsi8 793	Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.)
⊢ (ψ → ((ψ ∧ φ) → χ))    ⇒   ⊢ ((φ ∧ ψ) → χ)
Theorem	anabss7 794	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 19-Nov-2013.)
⊢ ((ψ ∧ (φ ∧ ψ)) → χ)    ⇒   ⊢ ((φ ∧ ψ) → χ)
Theorem	anabsan2 795	Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.)
⊢ ((φ ∧ (ψ ∧ ψ)) → χ)    ⇒   ⊢ ((φ ∧ ψ) → χ)
Theorem	anabss3 796	Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
⊢ (((φ ∧ ψ) ∧ ψ) → χ)    ⇒   ⊢ ((φ ∧ ψ) → χ)
Theorem	an4 797	Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) ↔ ((φ ∧ χ) ∧ (ψ ∧ θ)))
Theorem	an42 798	Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) ↔ ((φ ∧ χ) ∧ (θ ∧ ψ)))
Theorem	an4s 799	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) → τ)    ⇒   ⊢ (((φ ∧ χ) ∧ (ψ ∧ θ)) → τ)
Theorem	an42s 800	Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
⊢ (((φ ∧ ψ) ∧ (χ ∧ θ)) → τ)    ⇒   ⊢ (((φ ∧ χ) ∧ (θ ∧ ψ)) → τ)