P. 10 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 901-1000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bigolden 901	Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
|- (((ph /\ ps) <-> ph) <-> (ps <-> (ph \/ ps)))
Theorem	pm5.71 902	Theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.)
|- ((ps -> -. ch) -> (((ph \/ ps) /\ ch) <-> (ph /\ ch)))
Theorem	pm5.75 903	Theorem *5.75 of [WhiteheadRussell] p. 126. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2012.)
|- (((ch -> -. ps) /\ (ph <-> (ps \/ ch))) -> ((ph /\ -. ps) <-> ch))
Theorem	bimsc1 904	Removal of conjunct from one side of an equivalence. (Contributed by NM, 5-Aug-1993.)
|- (((ph -> ps) /\ (ch <-> (ps /\ ph))) -> (ch <-> ph))
Theorem	4exmid 905	The disjunction of the four possible combinations of two wffs and their negations is always true. (Contributed by David Abernethy, 28-Jan-2014.)
|- (((ph /\ ps) \/ (-. ph /\ -. ps)) \/ ((ph /\ -. ps) \/ (ps /\ -. ph)))
Theorem	ecase2d 906	Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Dec-2012.)
|- (ph -> ps)   &   |- (ph -> -. (ps /\ ch))   &   |- (ph -> -. (ps /\ th))   &   |- (ph -> (ta \/ (ch \/ th)))   =>   |- (ph -> ta)
Theorem	ecase3 907	Inference for elimination by cases. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
|- (ph -> ch)   &   |- (ps -> ch)   &   |- (-. (ph \/ ps) -> ch)   =>   |- ch
Theorem	ecase 908	Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)
|- (-. ph -> ch)   &   |- (-. ps -> ch)   &   |- ((ph /\ ps) -> ch)   =>   |- ch
Theorem	ecase3d 909	Deduction for elimination by cases. (Contributed by NM, 2-May-1996.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- (ph -> (ps -> th))   &   |- (ph -> (ch -> th))   &   |- (ph -> (-. (ps \/ ch) -> th))   =>   |- (ph -> th)
Theorem	ecased 910	Deduction for elimination by cases. (Contributed by NM, 8-Oct-2012.)
|- (ph -> (-. ps -> th))   &   |- (ph -> (-. ch -> th))   &   |- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> th)
Theorem	ecase3ad 911	Deduction for elimination by cases. (Contributed by NM, 24-May-2013.)
|- (ph -> (ps -> th))   &   |- (ph -> (ch -> th))   &   |- (ph -> ((-. ps /\ -. ch) -> th))   =>   |- (ph -> th)
Theorem	ccase 912	Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
|- ((ph /\ ps) -> ta)   &   |- ((ch /\ ps) -> ta)   &   |- ((ph /\ th) -> ta)   &   |- ((ch /\ th) -> ta)   =>   |- (((ph \/ ch) /\ (ps \/ th)) -> ta)
Theorem	ccased 913	Deduction for combining cases. (Contributed by NM, 9-May-2004.)
|- (ph -> ((ps /\ ch) -> et))   &   |- (ph -> ((th /\ ch) -> et))   &   |- (ph -> ((ps /\ ta) -> et))   &   |- (ph -> ((th /\ ta) -> et))   =>   |- (ph -> (((ps \/ th) /\ (ch \/ ta)) -> et))
Theorem	ccase2 914	Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
|- ((ph /\ ps) -> ta)   &   |- (ch -> ta)   &   |- (th -> ta)   =>   |- (((ph \/ ch) /\ (ps \/ th)) -> ta)
Theorem	4cases 915	Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003.)
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ -. ps) -> ch)   &   |- ((-. ph /\ ps) -> ch)   &   |- ((-. ph /\ -. ps) -> ch)   =>   |- ch
Theorem	4casesdan 916	Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013.)
|- ((ph /\ (ps /\ ch)) -> th)   &   |- ((ph /\ (ps /\ -. ch)) -> th)   &   |- ((ph /\ (-. ps /\ ch)) -> th)   &   |- ((ph /\ (-. ps /\ -. ch)) -> th)   =>   |- (ph -> th)
Theorem	niabn 917	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
|- ph   =>   |- (-. ps -> ((ch /\ ps) <-> -. ph))
Theorem	dedlem0a 918	Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
|- (ph -> (ps <-> ((ch -> ph) -> (ps /\ ph))))
Theorem	dedlem0b 919	Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.)
|- (-. ph -> (ps <-> ((ps -> ph) -> (ch /\ ph))))
Theorem	dedlema 920	Lemma for weak deduction theorem. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- (ph -> (ps <-> ((ps /\ ph) \/ (ch /\ -. ph))))
Theorem	dedlemb 921	Lemma for weak deduction theorem. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- (-. ph -> (ch <-> ((ps /\ ph) \/ (ch /\ -. ph))))
Theorem	elimh 922	Hypothesis builder for weak deduction theorem. For more information, see the Deduction Theorem link on the Metamath Proof Explorer home page. (Contributed by NM, 26-Jun-2002.)
|- ((ph <-> ((ph /\ ch) \/ (ps /\ -. ch))) -> (ch <-> ta))   &   |- ((ps <-> ((ph /\ ch) \/ (ps /\ -. ch))) -> (th <-> ta))   &   |- th   =>   |- ta
Theorem	dedt 923	The weak deduction theorem. For more information, see the Deduction Theorem link on the Metamath Proof Explorer home page. (Contributed by NM, 26-Jun-2002.)
|- ((ph <-> ((ph /\ ch) \/ (ps /\ -. ch))) -> (th <-> ta))   &   |- ta   =>   |- (ch -> th)
Theorem	con3th 924	Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. This version of con3 126 demonstrates the use of the weak deduction theorem dedt 923 to derive it from con3i 127. (Contributed by NM, 27-Jun-2002.) (Proof modification is discouraged.)
|- ((ph -> ps) -> (-. ps -> -. ph))
Theorem	consensus 925	The consensus theorem. This theorem and its dual (with \/ and /\ interchanged) are commonly used in computer logic design to eliminate redundant terms from Boolean expressions. Specifically, we prove that the term (ps /\ ch) on the left-hand side is redundant. (Contributed by NM, 16-May-2003.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 20-Jan-2013.)
|- ((((ph /\ ps) \/ (-. ph /\ ch)) \/ (ps /\ ch)) <-> ((ph /\ ps) \/ (-. ph /\ ch)))
Theorem	pm4.42 926	Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed by Roy F. Longton, 21-Jun-2005.)
|- (ph <-> ((ph /\ ps) \/ (ph /\ -. ps)))
Theorem	ninba 927	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
|- ph   =>   |- (-. ps -> (-. ph <-> (ch /\ ps)))
Theorem	prlem1 928	A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
|- (ph -> (et <-> ch))   &   |- (ps -> -. th)   =>   |- (ph -> (ps -> (((ps /\ ch) \/ (th /\ ta)) -> et)))
Theorem	prlem2 929	A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
|- (((ph /\ ps) \/ (ch /\ th)) <-> ((ph \/ ch) /\ ((ph /\ ps) \/ (ch /\ th))))
Theorem	oplem1 930	A specialized lemma for set theory (ordered pair theorem). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Wolf Lammen, 8-Dec-2012.)
|- (ph -> (ps \/ ch))   &   |- (ph -> (th \/ ta))   &   |- (ps <-> th)   &   |- (ch -> (th <-> ta))   =>   |- (ph -> ps)
Theorem	rnlem 931	Lemma used in construction of real numbers. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- (((ph /\ ps) /\ (ch /\ th)) <-> (((ph /\ ch) /\ (ps /\ th)) /\ ((ph /\ th) /\ (ps /\ ch))))
Theorem	dn1 932	A single axiom for Boolean algebra known as DN1. See http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf. (Contributed by Jeffrey Hankins, 3-Jul-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
|- (-. (-. (-. (ph \/ ps) \/ ch) \/ -. (ph \/ -. (-. ch \/ -. (ch \/ th)))) <-> ch)
1.2.8  Abbreviated conjunction and disjunction of three wff's
Syntax	w3o 933	Extend wff definition to include 3-way disjunction ('or').
wff (ph \/ ps \/ ch)
Syntax	w3a 934	Extend wff definition to include 3-way conjunction ('and').
wff (ph /\ ps /\ ch)
Definition	df-3or 935	Define disjunction ('or') of three wff's. Definition *2.33 of [WhiteheadRussell] p. 105. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law orass 510. (Contributed by NM, 8-Apr-1994.)
|- ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))
Definition	df-3an 936	Define conjunction ('and') of three wff's. Definition *4.34 of [WhiteheadRussell] p. 118. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law anass 630. (Contributed by NM, 8-Apr-1994.)
|- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
Theorem	3orass 937	Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
|- ((ph \/ ps \/ ch) <-> (ph \/ (ps \/ ch)))
Theorem	3anass 938	Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|- ((ph /\ ps /\ ch) <-> (ph /\ (ps /\ ch)))
Theorem	3anrot 939	Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|- ((ph /\ ps /\ ch) <-> (ps /\ ch /\ ph))
Theorem	3orrot 940	Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
|- ((ph \/ ps \/ ch) <-> (ps \/ ch \/ ph))
Theorem	3ancoma 941	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ((ph /\ ps /\ ch) <-> (ps /\ ph /\ ch))
Theorem	3orcoma 942	Commutation law for triple disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ((ph \/ ps \/ ch) <-> (ps \/ ph \/ ch))
Theorem	3ancomb 943	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ((ph /\ ps /\ ch) <-> (ph /\ ch /\ ps))
Theorem	3orcomb 944	Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.)
|- ((ph \/ ps \/ ch) <-> (ph \/ ch \/ ps))
Theorem	3anrev 945	Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ((ph /\ ps /\ ch) <-> (ch /\ ps /\ ph))
Theorem	3anan32 946	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ((ph /\ ps /\ ch) <-> ((ph /\ ch) /\ ps))
Theorem	3anan12 947	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ((ph /\ ps /\ ch) <-> (ps /\ (ph /\ ch)))
Theorem	3anor 948	Triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.)
|- ((ph /\ ps /\ ch) <-> -. (-. ph \/ -. ps \/ -. ch))
Theorem	3ianor 949	Negated triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- (-. (ph /\ ps /\ ch) <-> (-. ph \/ -. ps \/ -. ch))
Theorem	3ioran 950	Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)
|- (-. (ph \/ ps \/ ch) <-> (-. ph /\ -. ps /\ -. ch))
Theorem	3oran 951	Triple disjunction in terms of triple conjunction. (Contributed by NM, 8-Oct-2012.)
|- ((ph \/ ps \/ ch) <-> -. (-. ph /\ -. ps /\ -. ch))
Theorem	3simpa 952	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ((ph /\ ps /\ ch) -> (ph /\ ps))
Theorem	3simpb 953	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ((ph /\ ps /\ ch) -> (ph /\ ch))
Theorem	3simpc 954	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ((ph /\ ps /\ ch) -> (ps /\ ch))
Theorem	simp1 955	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ((ph /\ ps /\ ch) -> ph)
Theorem	simp2 956	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ((ph /\ ps /\ ch) -> ps)
Theorem	simp3 957	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ((ph /\ ps /\ ch) -> ch)
Theorem	simpl1 958	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- (((ph /\ ps /\ ch) /\ th) -> ph)
Theorem	simpl2 959	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- (((ph /\ ps /\ ch) /\ th) -> ps)
Theorem	simpl3 960	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- (((ph /\ ps /\ ch) /\ th) -> ch)
Theorem	simpr1 961	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ((ph /\ (ps /\ ch /\ th)) -> ps)
Theorem	simpr2 962	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ((ph /\ (ps /\ ch /\ th)) -> ch)
Theorem	simpr3 963	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ((ph /\ (ps /\ ch /\ th)) -> th)
Theorem	simp1i 964	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- (ph /\ ps /\ ch)   =>   |- ph
Theorem	simp2i 965	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- (ph /\ ps /\ ch)   =>   |- ps
Theorem	simp3i 966	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- (ph /\ ps /\ ch)   =>   |- ch
Theorem	simp1d 967	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- (ph -> (ps /\ ch /\ th))   =>   |- (ph -> ps)
Theorem	simp2d 968	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- (ph -> (ps /\ ch /\ th))   =>   |- (ph -> ch)
Theorem	simp3d 969	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- (ph -> (ps /\ ch /\ th))   =>   |- (ph -> th)
Theorem	simp1bi 970	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph <-> (ps /\ ch /\ th))   =>   |- (ph -> ps)
Theorem	simp2bi 971	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph <-> (ps /\ ch /\ th))   =>   |- (ph -> ch)
Theorem	simp3bi 972	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph <-> (ps /\ ch /\ th))   =>   |- (ph -> th)
Theorem	3adant1 973	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ((ph /\ ps) -> ch)   =>   |- ((th /\ ph /\ ps) -> ch)
Theorem	3adant2 974	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ((ph /\ ps) -> ch)   =>   |- ((ph /\ th /\ ps) -> ch)
Theorem	3adant3 975	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ((ph /\ ps) -> ch)   =>   |- ((ph /\ ps /\ th) -> ch)
Theorem	3ad2ant1 976	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- (ph -> ch)   =>   |- ((ph /\ ps /\ th) -> ch)
Theorem	3ad2ant2 977	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- (ph -> ch)   =>   |- ((ps /\ ph /\ th) -> ch)
Theorem	3ad2ant3 978	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- (ph -> ch)   =>   |- ((ps /\ th /\ ph) -> ch)
Theorem	simp1l 979	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- (((ph /\ ps) /\ ch /\ th) -> ph)
Theorem	simp1r 980	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- (((ph /\ ps) /\ ch /\ th) -> ps)
Theorem	simp2l 981	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ((ph /\ (ps /\ ch) /\ th) -> ps)
Theorem	simp2r 982	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ((ph /\ (ps /\ ch) /\ th) -> ch)
Theorem	simp3l 983	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ((ph /\ ps /\ (ch /\ th)) -> ch)
Theorem	simp3r 984	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ((ph /\ ps /\ (ch /\ th)) -> th)
Theorem	simp11 985	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- (((ph /\ ps /\ ch) /\ th /\ ta) -> ph)
Theorem	simp12 986	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- (((ph /\ ps /\ ch) /\ th /\ ta) -> ps)
Theorem	simp13 987	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- (((ph /\ ps /\ ch) /\ th /\ ta) -> ch)
Theorem	simp21 988	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ((ph /\ (ps /\ ch /\ th) /\ ta) -> ps)
Theorem	simp22 989	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ((ph /\ (ps /\ ch /\ th) /\ ta) -> ch)
Theorem	simp23 990	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ((ph /\ (ps /\ ch /\ th) /\ ta) -> th)
Theorem	simp31 991	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ((ph /\ ps /\ (ch /\ th /\ ta)) -> ch)
Theorem	simp32 992	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ((ph /\ ps /\ (ch /\ th /\ ta)) -> th)
Theorem	simp33 993	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ((ph /\ ps /\ (ch /\ th /\ ta)) -> ta)
Theorem	simpll1 994	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps /\ ch) /\ th) /\ ta) -> ph)
Theorem	simpll2 995	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps /\ ch) /\ th) /\ ta) -> ps)
Theorem	simpll3 996	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((((ph /\ ps /\ ch) /\ th) /\ ta) -> ch)
Theorem	simplr1 997	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ (ph /\ ps /\ ch)) /\ ta) -> ph)
Theorem	simplr2 998	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ (ph /\ ps /\ ch)) /\ ta) -> ps)
Theorem	simplr3 999	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- (((th /\ (ph /\ ps /\ ch)) /\ ta) -> ch)
Theorem	simprl1 1000	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ((ta /\ ((ph /\ ps /\ ch) /\ th)) -> ph)