P. 11 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1001-1100   *Has distinct variable group(s)

Type	Label	Description
Statement
1.2.12  Abbreviated conjunction and disjunction of three wff's
Syntax	w3o 1001	Extend wff definition to include 3-way disjunction ('or').
wff ( ph \/ ps \/ ch )
Syntax	w3a 1002	Extend wff definition to include 3-way conjunction ('and').
wff ( ph /\ ps /\ ch )
Definition	df-3or 1003	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 772. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
Definition	df-3an 1004	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 401. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
Theorem	3orass 1005	Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph \/ ps \/ ch ) <-> ( ph \/ ( ps \/ ch ) ) )
Theorem	3anass 1006	Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
Theorem	3anrot 1007	Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ch /\ ph ) )
Theorem	3orrot 1008	Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
|- ( ( ph \/ ps \/ ch ) <-> ( ps \/ ch \/ ph ) )
Theorem	3ancoma 1009	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ph /\ ch ) )
Theorem	3ancomb 1010	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ch /\ ps ) )
Theorem	3orcomb 1011	Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.)
|- ( ( ph \/ ps \/ ch ) <-> ( ph \/ ch \/ ps ) )
Theorem	3anrev 1012	Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ch /\ ps /\ ph ) )
Theorem	3anan32 1013	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ch ) /\ ps ) )
Theorem	3anan12 1014	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 1015	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
Theorem	anandi3r 1016	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ( ch /\ ps ) ) )
Theorem	3ioran 1017	Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)
|- ( -. ( ph \/ ps \/ ch ) <-> ( -. ph /\ -. ps /\ -. ch ) )
Theorem	3simpa 1018	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )
Theorem	3simpb 1019	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ( ph /\ ch ) )
Theorem	3simpc 1020	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 1021	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ph )
Theorem	simp2 1022	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ps )
Theorem	simp3 1023	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ch )
Theorem	simpl1 1024	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )
Theorem	simpl2 1025	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
Theorem	simpl3 1026	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )
Theorem	simpr1 1027	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ps )
Theorem	simpr2 1028	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ch )
Theorem	simpr3 1029	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> th )
Theorem	simp1i 1030	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- ( ph /\ ps /\ ch )   =>    |- ph
Theorem	simp2i 1031	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- ( ph /\ ps /\ ch )   =>    |- ps
Theorem	simp3i 1032	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- ( ph /\ ps /\ ch )   =>    |- ch
Theorem	simp1d 1033	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ps )
Theorem	simp2d 1034	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ch )
Theorem	simp3d 1035	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> th )
Theorem	simp1bi 1036	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ps )
Theorem	simp2bi 1037	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ch )
Theorem	simp3bi 1038	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> th )
Theorem	3adant1 1039	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( th /\ ph /\ ps ) -> ch )
Theorem	3adant2 1040	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ph /\ th /\ ps ) -> ch )
Theorem	3adant3 1041	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ph /\ ps /\ th ) -> ch )
Theorem	3ad2ant1 1042	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- ( ph -> ch )   =>    |- ( ( ph /\ ps /\ th ) -> ch )
Theorem	3ad2ant2 1043	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- ( ph -> ch )   =>    |- ( ( ps /\ ph /\ th ) -> ch )
Theorem	3ad2ant3 1044	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- ( ph -> ch )   =>    |- ( ( ps /\ th /\ ph ) -> ch )
Theorem	simp1l 1045	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ph )
Theorem	simp1r 1046	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )
Theorem	simp2l 1047	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )
Theorem	simp2r 1048	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ch )
Theorem	simp3l 1049	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th ) ) -> ch )
Theorem	simp3r 1050	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th ) ) -> th )
Theorem	simp11 1051	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ph )
Theorem	simp12 1052	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ps )
Theorem	simp13 1053	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ch )
Theorem	simp21 1054	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> ps )
Theorem	simp22 1055	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> ch )
Theorem	simp23 1056	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> th )
Theorem	simp31 1057	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th /\ ta ) ) -> ch )
Theorem	simp32 1058	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th /\ ta ) ) -> th )
Theorem	simp33 1059	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th /\ ta ) ) -> ta )
Theorem	simpll1 1060	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ph )
Theorem	simpll2 1061	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )
Theorem	simpll3 1062	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ch )
Theorem	simplr1 1063	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ph )
Theorem	simplr2 1064	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ps )
Theorem	simplr3 1065	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ch )
Theorem	simprl1 1066	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ph )
Theorem	simprl2 1067	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ps )
Theorem	simprl3 1068	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ch )
Theorem	simprr1 1069	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ph )
Theorem	simprr2 1070	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ps )
Theorem	simprr3 1071	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ch )
Theorem	simpl1l 1072	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta ) -> ph )
Theorem	simpl1r 1073	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta ) -> ps )
Theorem	simpl2l 1074	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta ) -> ph )
Theorem	simpl2r 1075	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta ) -> ps )
Theorem	simpl3l 1076	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta ) -> ph )
Theorem	simpl3r 1077	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta ) -> ps )
Theorem	simpr1l 1078	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps ) /\ ch /\ th ) ) -> ph )
Theorem	simpr1r 1079	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps ) /\ ch /\ th ) ) -> ps )
Theorem	simpr2l 1080	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ ( ph /\ ps ) /\ th ) ) -> ph )
Theorem	simpr2r 1081	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ ( ph /\ ps ) /\ th ) ) -> ps )
Theorem	simpr3l 1082	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ th /\ ( ph /\ ps ) ) ) -> ph )
Theorem	simpr3r 1083	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ th /\ ( ph /\ ps ) ) ) -> ps )
Theorem	simp1ll 1084	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th /\ ta ) -> ph )
Theorem	simp1lr 1085	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th /\ ta ) -> ps )
Theorem	simp1rl 1086	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) ) /\ th /\ ta ) -> ph )
Theorem	simp1rr 1087	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) ) /\ th /\ ta ) -> ps )
Theorem	simp2ll 1088	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ( ( ph /\ ps ) /\ ch ) /\ ta ) -> ph )
Theorem	simp2lr 1089	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ( ( ph /\ ps ) /\ ch ) /\ ta ) -> ps )
Theorem	simp2rl 1090	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ( ch /\ ( ph /\ ps ) ) /\ ta ) -> ph )
Theorem	simp2rr 1091	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ( ch /\ ( ph /\ ps ) ) /\ ta ) -> ps )
Theorem	simp3ll 1092	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ( ph /\ ps ) /\ ch ) ) -> ph )
Theorem	simp3lr 1093	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ( ph /\ ps ) /\ ch ) ) -> ps )
Theorem	simp3rl 1094	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ch /\ ( ph /\ ps ) ) ) -> ph )
Theorem	simp3rr 1095	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ch /\ ( ph /\ ps ) ) ) -> ps )
Theorem	simpl11 1096	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et ) -> ph )
Theorem	simpl12 1097	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et ) -> ps )
Theorem	simpl13 1098	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et ) -> ch )
Theorem	simpl21 1099	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et ) -> ph )
Theorem	simpl22 1100	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et ) -> ps )