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
Theorem	looinvdc 901	The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz, but where one of the propositions is decidable. Using dfor2dc 881, we can see that this expresses "disjunction commutes." Theorem *2.69 of [WhiteheadRussell] p. 108 (plus the decidability condition). (Contributed by NM, 12-Aug-2004.)
|- (DECID ph -> ( ( ( ph -> ps ) -> ps ) -> ( ( ps -> ph ) -> ph ) ) )
1.2.10  Miscellaneous theorems of propositional calculus
Theorem	pm5.21nd 902	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 903	Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) -> ( ph -> ( ps <-> ch ) ) )
Theorem	pm5.54dc 904	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 905	Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ph <-> ch ) )
Theorem	baibr 906	Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ch <-> ph ) )
Theorem	rbaib 907	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ch -> ( ph <-> ps ) )
Theorem	rbaibr 908	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ch -> ( ps <-> ph ) )
Theorem	baibd 909	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ ch ) -> ( ps <-> th ) )
Theorem	rbaibd 910	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ th ) -> ( ps <-> ch ) )
Theorem	pm5.44 911	Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) -> ( ( ph -> ch ) <-> ( ph -> ( ps /\ ch ) ) ) )
Theorem	pm5.6dc 912	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 913). (Contributed by Jim Kingdon, 2-Apr-2018.)
|- (DECID ps -> ( ( ( ph /\ -. ps ) -> ch ) <-> ( ph -> ( ps \/ ch ) ) ) )
Theorem	pm5.6r 913	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 912). (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( ph -> ( ps \/ ch ) ) -> ( ( ph /\ -. ps ) -> ch ) )
Theorem	orcanai 914	Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
|- ( ph -> ( ps \/ ch ) )   =>    |- ( ( ph /\ -. ps ) -> ch )
Theorem	intnan 915	Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
|- -. ph   =>    |- -. ( ps /\ ph )
Theorem	intnanr 916	Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
|- -. ph   =>    |- -. ( ph /\ ps )
Theorem	intnand 917	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. ( ch /\ ps ) )
Theorem	intnanrd 918	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. ( ps /\ ch ) )
Theorem	dcan 919	A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
|- (DECID ph -> (DECID ps -> DECID ( ph /\ ps ) ) )
Theorem	dcor 920	A disjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.)
|- (DECID ph -> (DECID ps -> DECID ( ph \/ ps ) ) )
Theorem	dcbi 921	An equivalence of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
|- (DECID ph -> (DECID ps -> DECID ( ph <-> ps ) ) )
Theorem	annimdc 922	Express conjunction in terms of implication. The forward direction, annimim 676, 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 923	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 924	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 925	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 926	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 927	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 928	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 929	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 930	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 931	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 932	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 933	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 934	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 935	Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> -. ps ) ) <-> -. ph )
Theorem	pm4.83dc 936	Theorem *4.83 of [WhiteheadRussell] p. 122, for decidable propositions. As with other case elimination theorems, like pm2.61dc 851, it only holds for decidable propositions. (Contributed by Jim Kingdon, 12-May-2018.)
|- (DECID ph -> ( ( ( ph -> ps ) /\ ( -. ph -> ps ) ) <-> ps ) )
Theorem	biantr 937	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 938	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 939	Disjunction distributes over the biconditional, for a decidable proposition. Based on theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbididc 938. (Contributed by Jim Kingdon, 2-Apr-2018.)
|- (DECID ch -> ( ( ( ph \/ ch ) <-> ( ps \/ ch ) ) <-> ( ch \/ ( ph <-> ps ) ) ) )
Theorem	bigolden 940	Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
|- ( ( ( ph /\ ps ) <-> ph ) <-> ( ps <-> ( ph \/ ps ) ) )
Theorem	anordc 941	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 744, 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 942	Theorem *3.11 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.1 744, 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 943	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 944	Theorem *3.13 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.14 743, holds for all propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
|- (DECID ph -> (DECID ps -> ( -. ( ph /\ ps ) -> ( -. ph \/ -. ps ) ) ) )
Theorem	dn1dc 945	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 946	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 947	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 948	Removal of conjunct from one side of an equivalence. (Contributed by NM, 5-Aug-1993.)
|- ( ( ( ph -> ps ) /\ ( ch <-> ( ps /\ ph ) ) ) -> ( ch <-> ph ) )
Theorem	ccase 949	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 950	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 951	Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
|- ( ( ph /\ ps ) -> ta )   &    |- ( ch -> ta )   &    |- ( th -> ta )   =>    |- ( ( ( ph \/ ch ) /\ ( ps \/ th ) ) -> ta )
Theorem	niabn 952	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
|- ph   =>    |- ( -. ps -> ( ( ch /\ ps ) <-> -. ph ) )
Theorem	dedlem0a 953	Alternate version of dedlema 954. (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 954	Lemma for iftrue 3510. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ( ph -> ( ps <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
Theorem	dedlemb 955	Lemma for iffalse 3513. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ( -. ph -> ( ch <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
Theorem	pm4.42r 956	One direction of Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( ( ph /\ ps ) \/ ( ph /\ -. ps ) ) -> ph )
Theorem	ninba 957	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
|- ph   =>    |- ( -. ps -> ( -. ph <-> ( ch /\ ps ) ) )
Theorem	prlem1 958	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 959	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 960	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 961	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 962	Extend wff definition to include 3-way disjunction ('or').
wff ( ph \/ ps \/ ch )
Syntax	w3a 963	Extend wff definition to include 3-way conjunction ('and').
wff ( ph /\ ps /\ ch )
Definition	df-3or 964	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 757. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
Definition	df-3an 965	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 399. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
Theorem	3orass 966	Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph \/ ps \/ ch ) <-> ( ph \/ ( ps \/ ch ) ) )
Theorem	3anass 967	Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
Theorem	3anrot 968	Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ch /\ ph ) )
Theorem	3orrot 969	Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
|- ( ( ph \/ ps \/ ch ) <-> ( ps \/ ch \/ ph ) )
Theorem	3ancoma 970	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ph /\ ch ) )
Theorem	3ancomb 971	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ch /\ ps ) )
Theorem	3orcomb 972	Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.)
|- ( ( ph \/ ps \/ ch ) <-> ( ph \/ ch \/ ps ) )
Theorem	3anrev 973	Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ch /\ ps /\ ph ) )
Theorem	3anan32 974	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ch ) /\ ps ) )
Theorem	3anan12 975	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 976	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
Theorem	anandi3r 977	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ( ch /\ ps ) ) )
Theorem	3ioran 978	Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)
|- ( -. ( ph \/ ps \/ ch ) <-> ( -. ph /\ -. ps /\ -. ch ) )
Theorem	3simpa 979	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )
Theorem	3simpb 980	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ( ph /\ ch ) )
Theorem	3simpc 981	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 982	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ph )
Theorem	simp2 983	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ps )
Theorem	simp3 984	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ch )
Theorem	simpl1 985	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )
Theorem	simpl2 986	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
Theorem	simpl3 987	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )
Theorem	simpr1 988	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ps )
Theorem	simpr2 989	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ch )
Theorem	simpr3 990	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> th )
Theorem	simp1i 991	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- ( ph /\ ps /\ ch )   =>    |- ph
Theorem	simp2i 992	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- ( ph /\ ps /\ ch )   =>    |- ps
Theorem	simp3i 993	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- ( ph /\ ps /\ ch )   =>    |- ch
Theorem	simp1d 994	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ps )
Theorem	simp2d 995	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ch )
Theorem	simp3d 996	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> th )
Theorem	simp1bi 997	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ps )
Theorem	simp2bi 998	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ch )
Theorem	simp3bi 999	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> th )
Theorem	3adant1 1000	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( th /\ ph /\ ps ) -> ch )