P. 10 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 901-1000   *Has distinct variable group(s)

Type	Label	Description
Statement
1.2.10  Miscellaneous theorems of propositional calculus
Theorem	pm5.21nd 901	Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.)
|- ( ( ph /\ ps ) -> th )   &    |- ( ( ph /\ ch ) -> th )   &    |- ( th -> ( ps <-> ch ) )   =>    |- ( ph -> ( ps <-> ch ) )
Theorem	pm5.35 902	Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) -> ( ph -> ( ps <-> ch ) ) )
Theorem	pm5.54dc 903	A conjunction is equivalent to one of its conjuncts, given a decidable conjunct. Based on theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by Jim Kingdon, 30-Mar-2018.)
|- (DECID ph -> ( ( ( ph /\ ps ) <-> ph ) \/ ( ( ph /\ ps ) <-> ps ) ) )
Theorem	baib 904	Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ph <-> ch ) )
Theorem	baibr 905	Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ch <-> ph ) )
Theorem	rbaib 906	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ch -> ( ph <-> ps ) )
Theorem	rbaibr 907	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ch -> ( ps <-> ph ) )
Theorem	baibd 908	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ ch ) -> ( ps <-> th ) )
Theorem	rbaibd 909	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ th ) -> ( ps <-> ch ) )
Theorem	pm5.44 910	Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) -> ( ( ph -> ch ) <-> ( ph -> ( ps /\ ch ) ) ) )
Theorem	pm5.6dc 911	Conjunction in antecedent versus disjunction in consequent, for a decidable proposition. Theorem *5.6 of [WhiteheadRussell] p. 125, with decidability condition added. The reverse implication holds for all propositions (see pm5.6r 912). (Contributed by Jim Kingdon, 2-Apr-2018.)
|- (DECID ps -> ( ( ( ph /\ -. ps ) -> ch ) <-> ( ph -> ( ps \/ ch ) ) ) )
Theorem	pm5.6r 912	Conjunction in antecedent versus disjunction in consequent. One direction of Theorem *5.6 of [WhiteheadRussell] p. 125. If ps is decidable, the converse also holds (see pm5.6dc 911). (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( ph -> ( ps \/ ch ) ) -> ( ( ph /\ -. ps ) -> ch ) )
Theorem	orcanai 913	Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
|- ( ph -> ( ps \/ ch ) )   =>    |- ( ( ph /\ -. ps ) -> ch )
Theorem	intnan 914	Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
|- -. ph   =>    |- -. ( ps /\ ph )
Theorem	intnanr 915	Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
|- -. ph   =>    |- -. ( ph /\ ps )
Theorem	intnand 916	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. ( ch /\ ps ) )
Theorem	intnanrd 917	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. ( ps /\ ch ) )
Theorem	dcan 918	A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
|- (DECID ph -> (DECID ps -> DECID ( ph /\ ps ) ) )
Theorem	dcor 919	A disjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.)
|- (DECID ph -> (DECID ps -> DECID ( ph \/ ps ) ) )
Theorem	dcbi 920	An equivalence of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
|- (DECID ph -> (DECID ps -> DECID ( ph <-> ps ) ) )
Theorem	annimdc 921	Express conjunction in terms of implication. The forward direction, annimim 675, is valid for all propositions, but as an equivalence, it requires a decidability condition. (Contributed by Jim Kingdon, 25-Apr-2018.)
|- (DECID ph -> (DECID ps -> ( ( ph /\ -. ps ) <-> -. ( ph -> ps ) ) ) )
Theorem	pm4.55dc 922	Theorem *4.55 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 2-May-2018.)
|- (DECID ph -> (DECID ps -> ( -. ( -. ph /\ ps ) <-> ( ph \/ -. ps ) ) ) )
Theorem	orandc 923	Disjunction in terms of conjunction (De Morgan's law), for decidable propositions. Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by Jim Kingdon, 13-Dec-2021.)
|- ( (DECID ph /\ DECID ps ) -> ( ( ph \/ ps ) <-> -. ( -. ph /\ -. ps ) ) )
Theorem	mpbiran 924	Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) (Revised by NM, 9-Jan-2015.)
|- ps   &    |- ( ph <-> ( ps /\ ch ) )   =>    |- ( ph <-> ch )
Theorem	mpbiran2 925	Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.)
|- ch   &    |- ( ph <-> ( ps /\ ch ) )   =>    |- ( ph <-> ps )
Theorem	mpbir2an 926	Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) (Revised by NM, 9-Jan-2015.)
|- ps   &    |- ch   &    |- ( ph <-> ( ps /\ ch ) )   =>    |- ph
Theorem	mpbi2and 927	Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> ( ( ps /\ ch ) <-> th ) )   =>    |- ( ph -> th )
Theorem	mpbir2and 928	Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ph -> ps )
Theorem	pm5.62dc 929	Theorem *5.62 of [WhiteheadRussell] p. 125, for a decidable proposition. (Contributed by Jim Kingdon, 12-May-2018.)
|- (DECID ps -> ( ( ( ph /\ ps ) \/ -. ps ) <-> ( ph \/ -. ps ) ) )
Theorem	pm5.63dc 930	Theorem *5.63 of [WhiteheadRussell] p. 125, for a decidable proposition. (Contributed by Jim Kingdon, 12-May-2018.)
|- (DECID ph -> ( ( ph \/ ps ) <-> ( ph \/ ( -. ph /\ ps ) ) ) )
Theorem	bianfi 931	A wff conjoined with falsehood is false. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
|- -. ph   =>    |- ( ph <-> ( ps /\ ph ) )
Theorem	bianfd 932	A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.)
|- ( ph -> -. ps )   =>    |- ( ph -> ( ps <-> ( ps /\ ch ) ) )
Theorem	pm4.43 933	Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
|- ( ph <-> ( ( ph \/ ps ) /\ ( ph \/ -. ps ) ) )
Theorem	pm4.82 934	Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> -. ps ) ) <-> -. ph )
Theorem	pm4.83dc 935	Theorem *4.83 of [WhiteheadRussell] p. 122, for decidable propositions. As with other case elimination theorems, like pm2.61dc 850, it only holds for decidable propositions. (Contributed by Jim Kingdon, 12-May-2018.)
|- (DECID ph -> ( ( ( ph -> ps ) /\ ( -. ph -> ps ) ) <-> ps ) )
Theorem	biantr 936	A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.)
|- ( ( ( ph <-> ps ) /\ ( ch <-> ps ) ) -> ( ph <-> ch ) )
Theorem	orbididc 937	Disjunction distributes over the biconditional, for a decidable proposition. Based on an axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.3384. (Contributed by Jim Kingdon, 2-Apr-2018.)
|- (DECID ph -> ( ( ph \/ ( ps <-> ch ) ) <-> ( ( ph \/ ps ) <-> ( ph \/ ch ) ) ) )
Theorem	pm5.7dc 938	Disjunction distributes over the biconditional, for a decidable proposition. Based on theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbididc 937. (Contributed by Jim Kingdon, 2-Apr-2018.)
|- (DECID ch -> ( ( ( ph \/ ch ) <-> ( ps \/ ch ) ) <-> ( ch \/ ( ph <-> ps ) ) ) )
Theorem	bigolden 939	Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
|- ( ( ( ph /\ ps ) <-> ph ) <-> ( ps <-> ( ph \/ ps ) ) )
Theorem	anordc 940	Conjunction in terms of disjunction (DeMorgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120, but where the propositions are decidable. The forward direction, pm3.1 743, holds for all propositions, but the equivalence only holds given decidability. (Contributed by Jim Kingdon, 21-Apr-2018.)
|- (DECID ph -> (DECID ps -> ( ( ph /\ ps ) <-> -. ( -. ph \/ -. ps ) ) ) )
Theorem	pm3.11dc 941	Theorem *3.11 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.1 743, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 22-Apr-2018.)
|- (DECID ph -> (DECID ps -> ( -. ( -. ph \/ -. ps ) -> ( ph /\ ps ) ) ) )
Theorem	pm3.12dc 942	Theorem *3.12 of [WhiteheadRussell] p. 111, but for decidable propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
|- (DECID ph -> (DECID ps -> ( ( -. ph \/ -. ps ) \/ ( ph /\ ps ) ) ) )
Theorem	pm3.13dc 943	Theorem *3.13 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.14 742, holds for all propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
|- (DECID ph -> (DECID ps -> ( -. ( ph /\ ps ) -> ( -. ph \/ -. ps ) ) ) )
Theorem	dn1dc 944	DN1 for decidable propositions. Without the decidability conditions, DN1 can serve as a single axiom for Boolean algebra. See http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf. (Contributed by Jim Kingdon, 22-Apr-2018.)
|- ( (DECID ph /\ (DECID ps /\ (DECID ch /\ DECID th ) ) ) -> ( -. ( -. ( -. ( ph \/ ps ) \/ ch ) \/ -. ( ph \/ -. ( -. ch \/ -. ( ch \/ th ) ) ) ) <-> ch ) )
Theorem	pm5.71dc 945	Decidable proposition version of theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.) (Modified for decidability by Jim Kingdon, 19-Apr-2018.)
|- (DECID ps -> ( ( ps -> -. ch ) -> ( ( ( ph \/ ps ) /\ ch ) <-> ( ph /\ ch ) ) ) )
Theorem	pm5.75 946	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 947	Removal of conjunct from one side of an equivalence. (Contributed by NM, 5-Aug-1993.)
|- ( ( ( ph -> ps ) /\ ( ch <-> ( ps /\ ph ) ) ) -> ( ch <-> ph ) )
Theorem	ccase 948	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 949	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 950	Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
|- ( ( ph /\ ps ) -> ta )   &    |- ( ch -> ta )   &    |- ( th -> ta )   =>    |- ( ( ( ph \/ ch ) /\ ( ps \/ th ) ) -> ta )
Theorem	niabn 951	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
|- ph   =>    |- ( -. ps -> ( ( ch /\ ps ) <-> -. ph ) )
Theorem	dedlem0a 952	Alternate version of dedlema 953. (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	dedlema 953	Lemma for iftrue 3474. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ( ph -> ( ps <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
Theorem	dedlemb 954	Lemma for iffalse 3477. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ( -. ph -> ( ch <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
Theorem	pm4.42r 955	One direction of Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( ( ph /\ ps ) \/ ( ph /\ -. ps ) ) -> ph )
Theorem	ninba 956	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
|- ph   =>    |- ( -. ps -> ( -. ph <-> ( ch /\ ps ) ) )
Theorem	prlem1 957	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 958	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 959	A specialized lemma for set theory (ordered pair theorem). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Wolf Lammen, 8-Dec-2012.) (Proof shortened by Mario Carneiro, 2-Feb-2015.)
|- ( ph -> ( ps \/ ch ) )   &    |- ( ph -> ( th \/ ta ) )   &    |- ( ps <-> th )   &    |- ( ch -> ( th <-> ta ) )   =>    |- ( ph -> ps )
Theorem	rnlem 960	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 ) ) ) )
1.2.11  Abbreviated conjunction and disjunction of three wff's
Syntax	w3o 961	Extend wff definition to include 3-way disjunction ('or').
wff ( ph \/ ps \/ ch )
Syntax	w3a 962	Extend wff definition to include 3-way conjunction ('and').
wff ( ph /\ ps /\ ch )
Definition	df-3or 963	Define disjunction ('or') of 3 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 756. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
Definition	df-3an 964	Define conjunction ('and') of 3 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 398. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
Theorem	3orass 965	Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph \/ ps \/ ch ) <-> ( ph \/ ( ps \/ ch ) ) )
Theorem	3anass 966	Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
Theorem	3anrot 967	Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ch /\ ph ) )
Theorem	3orrot 968	Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
|- ( ( ph \/ ps \/ ch ) <-> ( ps \/ ch \/ ph ) )
Theorem	3ancoma 969	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ph /\ ch ) )
Theorem	3ancomb 970	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ch /\ ps ) )
Theorem	3orcomb 971	Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.)
|- ( ( ph \/ ps \/ ch ) <-> ( ph \/ ch \/ ps ) )
Theorem	3anrev 972	Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ch /\ ps /\ ph ) )
Theorem	3anan32 973	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ch ) /\ ps ) )
Theorem	3anan12 974	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	anandi3 975	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
Theorem	anandi3r 976	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ( ch /\ ps ) ) )
Theorem	3ioran 977	Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)
|- ( -. ( ph \/ ps \/ ch ) <-> ( -. ph /\ -. ps /\ -. ch ) )
Theorem	3simpa 978	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )
Theorem	3simpb 979	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ( ph /\ ch ) )
Theorem	3simpc 980	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 981	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ph )
Theorem	simp2 982	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ps )
Theorem	simp3 983	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ch )
Theorem	simpl1 984	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )
Theorem	simpl2 985	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
Theorem	simpl3 986	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )
Theorem	simpr1 987	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ps )
Theorem	simpr2 988	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ch )
Theorem	simpr3 989	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> th )
Theorem	simp1i 990	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- ( ph /\ ps /\ ch )   =>    |- ph
Theorem	simp2i 991	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- ( ph /\ ps /\ ch )   =>    |- ps
Theorem	simp3i 992	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- ( ph /\ ps /\ ch )   =>    |- ch
Theorem	simp1d 993	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ps )
Theorem	simp2d 994	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ch )
Theorem	simp3d 995	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> th )
Theorem	simp1bi 996	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ps )
Theorem	simp2bi 997	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ch )
Theorem	simp3bi 998	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> th )
Theorem	3adant1 999	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( th /\ ph /\ ps ) -> ch )
Theorem	3adant2 1000	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ph /\ th /\ ps ) -> ch )