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	simp3d 1001	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
|- ( ph -> ( ps /\ ch /\ th ) )   =>    |- ( ph -> th )
Theorem	simp1bi 1002	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ps )
Theorem	simp2bi 1003	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ch )
Theorem	simp3bi 1004	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> th )
Theorem	3adant1 1005	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( th /\ ph /\ ps ) -> ch )
Theorem	3adant2 1006	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ph /\ th /\ ps ) -> ch )
Theorem	3adant3 1007	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
|- ( ( ph /\ ps ) -> ch )   =>    |- ( ( ph /\ ps /\ th ) -> ch )
Theorem	3ad2ant1 1008	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- ( ph -> ch )   =>    |- ( ( ph /\ ps /\ th ) -> ch )
Theorem	3ad2ant2 1009	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- ( ph -> ch )   =>    |- ( ( ps /\ ph /\ th ) -> ch )
Theorem	3ad2ant3 1010	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
|- ( ph -> ch )   =>    |- ( ( ps /\ th /\ ph ) -> ch )
Theorem	simp1l 1011	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ph )
Theorem	simp1r 1012	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ps )
Theorem	simp2l 1013	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ps )
Theorem	simp2r 1014	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch ) /\ th ) -> ch )
Theorem	simp3l 1015	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th ) ) -> ch )
Theorem	simp3r 1016	Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th ) ) -> th )
Theorem	simp11 1017	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ph )
Theorem	simp12 1018	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ps )
Theorem	simp13 1019	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ch )
Theorem	simp21 1020	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> ps )
Theorem	simp22 1021	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> ch )
Theorem	simp23 1022	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ( ps /\ ch /\ th ) /\ ta ) -> th )
Theorem	simp31 1023	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th /\ ta ) ) -> ch )
Theorem	simp32 1024	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th /\ ta ) ) -> th )
Theorem	simp33 1025	Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)
|- ( ( ph /\ ps /\ ( ch /\ th /\ ta ) ) -> ta )
Theorem	simpll1 1026	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ph )
Theorem	simpll2 1027	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )
Theorem	simpll3 1028	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ch )
Theorem	simplr1 1029	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ph )
Theorem	simplr2 1030	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ps )
Theorem	simplr3 1031	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta ) -> ch )
Theorem	simprl1 1032	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ph )
Theorem	simprl2 1033	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ps )
Theorem	simprl3 1034	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ch )
Theorem	simprr1 1035	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ph )
Theorem	simprr2 1036	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ps )
Theorem	simprr3 1037	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ch )
Theorem	simpl1l 1038	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta ) -> ph )
Theorem	simpl1r 1039	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta ) -> ps )
Theorem	simpl2l 1040	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta ) -> ph )
Theorem	simpl2r 1041	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta ) -> ps )
Theorem	simpl3l 1042	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta ) -> ph )
Theorem	simpl3r 1043	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta ) -> ps )
Theorem	simpr1l 1044	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps ) /\ ch /\ th ) ) -> ph )
Theorem	simpr1r 1045	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps ) /\ ch /\ th ) ) -> ps )
Theorem	simpr2l 1046	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ ( ph /\ ps ) /\ th ) ) -> ph )
Theorem	simpr2r 1047	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ ( ph /\ ps ) /\ th ) ) -> ps )
Theorem	simpr3l 1048	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ th /\ ( ph /\ ps ) ) ) -> ph )
Theorem	simpr3r 1049	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ th /\ ( ph /\ ps ) ) ) -> ps )
Theorem	simp1ll 1050	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th /\ ta ) -> ph )
Theorem	simp1lr 1051	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th /\ ta ) -> ps )
Theorem	simp1rl 1052	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) ) /\ th /\ ta ) -> ph )
Theorem	simp1rr 1053	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) ) /\ th /\ ta ) -> ps )
Theorem	simp2ll 1054	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ( ( ph /\ ps ) /\ ch ) /\ ta ) -> ph )
Theorem	simp2lr 1055	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ( ( ph /\ ps ) /\ ch ) /\ ta ) -> ps )
Theorem	simp2rl 1056	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ( ch /\ ( ph /\ ps ) ) /\ ta ) -> ph )
Theorem	simp2rr 1057	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ( ch /\ ( ph /\ ps ) ) /\ ta ) -> ps )
Theorem	simp3ll 1058	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ( ph /\ ps ) /\ ch ) ) -> ph )
Theorem	simp3lr 1059	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ( ph /\ ps ) /\ ch ) ) -> ps )
Theorem	simp3rl 1060	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ch /\ ( ph /\ ps ) ) ) -> ph )
Theorem	simp3rr 1061	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ch /\ ( ph /\ ps ) ) ) -> ps )
Theorem	simpl11 1062	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et ) -> ph )
Theorem	simpl12 1063	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et ) -> ps )
Theorem	simpl13 1064	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et ) -> ch )
Theorem	simpl21 1065	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et ) -> ph )
Theorem	simpl22 1066	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et ) -> ps )
Theorem	simpl23 1067	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et ) -> ch )
Theorem	simpl31 1068	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ph )
Theorem	simpl32 1069	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ps )
Theorem	simpl33 1070	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ch )
Theorem	simpr11 1071	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ph )
Theorem	simpr12 1072	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ps )
Theorem	simpr13 1073	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ch )
Theorem	simpr21 1074	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ph )
Theorem	simpr22 1075	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ps )
Theorem	simpr23 1076	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ch )
Theorem	simpr31 1077	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ph )
Theorem	simpr32 1078	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ps )
Theorem	simpr33 1079	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ch )
Theorem	simp1l1 1080	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta /\ et ) -> ph )
Theorem	simp1l2 1081	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta /\ et ) -> ps )
Theorem	simp1l3 1082	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta /\ et ) -> ch )
Theorem	simp1r1 1083	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta /\ et ) -> ph )
Theorem	simp1r2 1084	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta /\ et ) -> ps )
Theorem	simp1r3 1085	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta /\ et ) -> ch )
Theorem	simp2l1 1086	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) /\ et ) -> ph )
Theorem	simp2l2 1087	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) /\ et ) -> ps )
Theorem	simp2l3 1088	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) /\ et ) -> ch )
Theorem	simp2r1 1089	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ph )
Theorem	simp2r2 1090	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ps )
Theorem	simp2r3 1091	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ch )
Theorem	simp3l1 1092	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ph )
Theorem	simp3l2 1093	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ps )
Theorem	simp3l3 1094	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ch )
Theorem	simp3r1 1095	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ph )
Theorem	simp3r2 1096	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ps )
Theorem	simp3r3 1097	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ch )
Theorem	simp11l 1098	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta /\ et ) -> ph )
Theorem	simp11r 1099	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta /\ et ) -> ps )
Theorem	simp12l 1100	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta /\ et ) -> ph )