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
Theorem	ifpnst 1001	Conditional operator for the negation of a proposition. (Contributed by BJ, 30-Sep-2019.) (Proof shortened by Wolf Lammen, 5-May-2024.)
|- (STAB ph -> (if- ( ph , ps , ch ) <-> if- ( -. ph , ch , ps ) ) )
Theorem	ifptru 1002	Value of the conditional operator for propositions when its first argument is true. Analogue for propositions of iftrue 3642. This is essentially dedlema 982. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 10-Jul-2020.)
|- ( ph -> (if- ( ph , ps , ch ) <-> ps ) )
Theorem	ifpfal 1003	Value of the conditional operator for propositions when its first argument is false. Analogue for propositions of iffalse 3645. This is essentially dedlemb 983. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 25-Jun-2020.)
|- ( -. ph -> (if- ( ph , ps , ch ) <-> ch ) )
Theorem	ifpiddc 1004	Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of ifiddc 3673. (Contributed by BJ, 20-Sep-2019.)
|- (DECID ph -> (if- ( ph , ps , ps ) <-> ps ) )
Theorem	ifpbi123d 1005	Equivalence deduction for conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 17-Apr-2024.)
|- ( ph -> ( ps <-> ta ) )   &    |- ( ph -> ( ch <-> et ) )   &    |- ( ph -> ( th <-> ze ) )   =>    |- ( ph -> (if- ( ps , ch , th ) <-> if- ( ta , et , ze ) ) )
Theorem	ifpbi23d 1006	Equivalence deduction for conditional operator for propositions. Convenience theorem for a frequent case. (Contributed by Wolf Lammen, 28-Apr-2024.)
|- ( ph -> ( ch <-> et ) )   &    |- ( ph -> ( th <-> ze ) )   =>    |- ( ph -> (if- ( ps , ch , th ) <-> if- ( ps , et , ze ) ) )
Theorem	1fpid3 1007	The value of the conditional operator for propositions is its third argument if the first and second argument imply the third argument. (Contributed by AV, 4-Apr-2021.)
|- ( ( ph /\ ps ) -> ch )   =>    |- (if- ( ph , ps , ch ) -> ch )
1.2.12  Abbreviated conjunction and disjunction of three wff's
Syntax	w3o 1008	Extend wff definition to include 3-way disjunction ('or').
wff ( ph \/ ps \/ ch )
Syntax	w3a 1009	Extend wff definition to include 3-way conjunction ('and').
wff ( ph /\ ps /\ ch )
Definition	df-3or 1010	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 779. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
Definition	df-3an 1011	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 405. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
Theorem	3orass 1012	Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph \/ ps \/ ch ) <-> ( ph \/ ( ps \/ ch ) ) )
Theorem	3anass 1013	Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ( ps /\ ch ) ) )
Theorem	3anrot 1014	Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ch /\ ph ) )
Theorem	3orrot 1015	Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
|- ( ( ph \/ ps \/ ch ) <-> ( ps \/ ch \/ ph ) )
Theorem	3ancoma 1016	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ph /\ ch ) )
Theorem	3ancomb 1017	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ph /\ ch /\ ps ) )
Theorem	3orcomb 1018	Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.)
|- ( ( ph \/ ps \/ ch ) <-> ( ph \/ ch \/ ps ) )
Theorem	3anrev 1019	Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) <-> ( ch /\ ps /\ ph ) )
Theorem	3anan32 1020	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ch ) /\ ps ) )
Theorem	3anan12 1021	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 1022	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
Theorem	anandi3r 1023	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ( ch /\ ps ) ) )
Theorem	3ioran 1024	Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)
|- ( -. ( ph \/ ps \/ ch ) <-> ( -. ph /\ -. ps /\ -. ch ) )
Theorem	3simpa 1025	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ( ph /\ ps ) )
Theorem	3simpb 1026	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ( ph /\ ch ) )
Theorem	3simpc 1027	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 1028	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ph )
Theorem	simp2 1029	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ps )
Theorem	simp3 1030	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ( ph /\ ps /\ ch ) -> ch )
Theorem	simpl1 1031	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )
Theorem	simpl2 1032	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
Theorem	simpl3 1033	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ch )
Theorem	simpr1 1034	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ps )
Theorem	simpr2 1035	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ch )
Theorem	simpr3 1036	Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|- ( ( ph /\ ( ps /\ ch /\ th ) ) -> th )
Theorem	simp1i 1037	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- ( ph /\ ps /\ ch )   =>    |- ph
Theorem	simp2i 1038	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- ( ph /\ ps /\ ch )   =>    |- ps
Theorem	simp3i 1039	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
|- ( ph /\ ps /\ ch )   =>    |- ch
Theorem	simp1d 1040	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ps )
Theorem	simp2d 1041	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ch )
Theorem	simp3d 1042	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> th )
Theorem	simp1bi 1043	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ps )
Theorem	simp2bi 1044	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ch )
Theorem	simp3bi 1045	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> th )
Theorem	3adant1 1046	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( th /\ ph /\ ps ) -> ch )
Theorem	3adant2 1047	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ph /\ th /\ ps ) -> ch )
Theorem	3adant3 1048	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ph /\ ps /\ th ) -> ch )
Theorem	3ad2ant1 1049	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- ( ph -> ch )   =>    |- ( ( ph /\ ps /\ th ) -> ch )
Theorem	3ad2ant2 1050	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- ( ph -> ch )   =>    |- ( ( ps /\ ph /\ th ) -> ch )
Theorem	3ad2ant3 1051	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- ( ph -> ch )   =>    |- ( ( ps /\ th /\ ph ) -> ch )
Theorem	simp1l 1052	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ph )
Theorem	simp1r 1053	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )
Theorem	simp2l 1054	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )
Theorem	simp2r 1055	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ch )
Theorem	simp3l 1056	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th ) ) -> ch )
Theorem	simp3r 1057	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th ) ) -> th )
Theorem	simp11 1058	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ph )
Theorem	simp12 1059	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ps )
Theorem	simp13 1060	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ch )
Theorem	simp21 1061	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> ps )
Theorem	simp22 1062	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> ch )
Theorem	simp23 1063	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> th )
Theorem	simp31 1064	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th /\ ta ) ) -> ch )
Theorem	simp32 1065	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th /\ ta ) ) -> th )
Theorem	simp33 1066	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th /\ ta ) ) -> ta )
Theorem	simpll1 1067	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ph )
Theorem	simpll2 1068	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )
Theorem	simpll3 1069	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ch )
Theorem	simplr1 1070	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ph )
Theorem	simplr2 1071	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ps )
Theorem	simplr3 1072	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ch )
Theorem	simprl1 1073	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ph )
Theorem	simprl2 1074	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ps )
Theorem	simprl3 1075	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ch )
Theorem	simprr1 1076	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ph )
Theorem	simprr2 1077	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ps )
Theorem	simprr3 1078	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ch )
Theorem	simpl1l 1079	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta ) -> ph )
Theorem	simpl1r 1080	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta ) -> ps )
Theorem	simpl2l 1081	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta ) -> ph )
Theorem	simpl2r 1082	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta ) -> ps )
Theorem	simpl3l 1083	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta ) -> ph )
Theorem	simpl3r 1084	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta ) -> ps )
Theorem	simpr1l 1085	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps ) /\ ch /\ th ) ) -> ph )
Theorem	simpr1r 1086	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps ) /\ ch /\ th ) ) -> ps )
Theorem	simpr2l 1087	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ ( ph /\ ps ) /\ th ) ) -> ph )
Theorem	simpr2r 1088	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ ( ph /\ ps ) /\ th ) ) -> ps )
Theorem	simpr3l 1089	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ th /\ ( ph /\ ps ) ) ) -> ph )
Theorem	simpr3r 1090	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ th /\ ( ph /\ ps ) ) ) -> ps )
Theorem	simp1ll 1091	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th /\ ta ) -> ph )
Theorem	simp1lr 1092	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th /\ ta ) -> ps )
Theorem	simp1rl 1093	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) ) /\ th /\ ta ) -> ph )
Theorem	simp1rr 1094	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) ) /\ th /\ ta ) -> ps )
Theorem	simp2ll 1095	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ( ( ph /\ ps ) /\ ch ) /\ ta ) -> ph )
Theorem	simp2lr 1096	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ( ( ph /\ ps ) /\ ch ) /\ ta ) -> ps )
Theorem	simp2rl 1097	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ( ch /\ ( ph /\ ps ) ) /\ ta ) -> ph )
Theorem	simp2rr 1098	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ( ch /\ ( ph /\ ps ) ) /\ ta ) -> ps )
Theorem	simp3ll 1099	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ( ph /\ ps ) /\ ch ) ) -> ph )
Theorem	simp3lr 1100	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ( ph /\ ps ) /\ ch ) ) -> ps )