P. 12 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 1101-1200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	simp3ll 1101	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ( ph /\ ps ) /\ ch ) ) -> ph )
Theorem	simp3lr 1102	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ( ph /\ ps ) /\ ch ) ) -> ps )
Theorem	simp3rl 1103	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ch /\ ( ph /\ ps ) ) ) -> ph )
Theorem	simp3rr 1104	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( th /\ ta /\ ( ch /\ ( ph /\ ps ) ) ) -> ps )
Theorem	simpl11 1105	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et ) -> ph )
Theorem	simpl12 1106	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et ) -> ps )
Theorem	simpl13 1107	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et ) -> ch )
Theorem	simpl21 1108	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et ) -> ph )
Theorem	simpl22 1109	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et ) -> ps )
Theorem	simpl23 1110	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et ) -> ch )
Theorem	simpl31 1111	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ph )
Theorem	simpl32 1112	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ps )
Theorem	simpl33 1113	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ch )
Theorem	simpr11 1114	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ph )
Theorem	simpr12 1115	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ps )
Theorem	simpr13 1116	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ch )
Theorem	simpr21 1117	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ph )
Theorem	simpr22 1118	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ps )
Theorem	simpr23 1119	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ch )
Theorem	simpr31 1120	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ph )
Theorem	simpr32 1121	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ps )
Theorem	simpr33 1122	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ch )
Theorem	simp1l1 1123	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta /\ et ) -> ph )
Theorem	simp1l2 1124	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta /\ et ) -> ps )
Theorem	simp1l3 1125	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta /\ et ) -> ch )
Theorem	simp1r1 1126	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta /\ et ) -> ph )
Theorem	simp1r2 1127	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta /\ et ) -> ps )
Theorem	simp1r3 1128	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) ) /\ ta /\ et ) -> ch )
Theorem	simp2l1 1129	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) /\ et ) -> ph )
Theorem	simp2l2 1130	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) /\ et ) -> ps )
Theorem	simp2l3 1131	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps /\ ch ) /\ th ) /\ et ) -> ch )
Theorem	simp2r1 1132	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ph )
Theorem	simp2r2 1133	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ps )
Theorem	simp2r3 1134	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ch )
Theorem	simp3l1 1135	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ph )
Theorem	simp3l2 1136	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ps )
Theorem	simp3l3 1137	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ch )
Theorem	simp3r1 1138	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ph )
Theorem	simp3r2 1139	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ps )
Theorem	simp3r3 1140	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ch )
Theorem	simp11l 1141	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta /\ et ) -> ph )
Theorem	simp11r 1142	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta /\ et ) -> ps )
Theorem	simp12l 1143	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta /\ et ) -> ph )
Theorem	simp12r 1144	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta /\ et ) -> ps )
Theorem	simp13l 1145	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta /\ et ) -> ph )
Theorem	simp13r 1146	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta /\ et ) -> ps )
Theorem	simp21l 1147	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps ) /\ ch /\ th ) /\ et ) -> ph )
Theorem	simp21r 1148	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps ) /\ ch /\ th ) /\ et ) -> ps )
Theorem	simp22l 1149	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ ( ph /\ ps ) /\ th ) /\ et ) -> ph )
Theorem	simp22r 1150	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ ( ph /\ ps ) /\ th ) /\ et ) -> ps )
Theorem	simp23l 1151	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ th /\ ( ph /\ ps ) ) /\ et ) -> ph )
Theorem	simp23r 1152	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ th /\ ( ph /\ ps ) ) /\ et ) -> ps )
Theorem	simp31l 1153	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ( ph /\ ps ) /\ ch /\ th ) ) -> ph )
Theorem	simp31r 1154	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ( ph /\ ps ) /\ ch /\ th ) ) -> ps )
Theorem	simp32l 1155	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ch /\ ( ph /\ ps ) /\ th ) ) -> ph )
Theorem	simp32r 1156	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ch /\ ( ph /\ ps ) /\ th ) ) -> ps )
Theorem	simp33l 1157	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ch /\ th /\ ( ph /\ ps ) ) ) -> ph )
Theorem	simp33r 1158	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ch /\ th /\ ( ph /\ ps ) ) ) -> ps )
Theorem	simp111 1159	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et /\ ze ) -> ph )
Theorem	simp112 1160	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et /\ ze ) -> ps )
Theorem	simp113 1161	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et /\ ze ) -> ch )
Theorem	simp121 1162	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et /\ ze ) -> ph )
Theorem	simp122 1163	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et /\ ze ) -> ps )
Theorem	simp123 1164	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et /\ ze ) -> ch )
Theorem	simp131 1165	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et /\ ze ) -> ph )
Theorem	simp132 1166	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et /\ ze ) -> ps )
Theorem	simp133 1167	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et /\ ze ) -> ch )
Theorem	simp211 1168	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ ze ) -> ph )
Theorem	simp212 1169	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ ze ) -> ps )
Theorem	simp213 1170	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ ze ) -> ch )
Theorem	simp221 1171	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ ze ) -> ph )
Theorem	simp222 1172	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ ze ) -> ps )
Theorem	simp223 1173	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ ze ) -> ch )
Theorem	simp231 1174	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ ze ) -> ph )
Theorem	simp232 1175	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ ze ) -> ps )
Theorem	simp233 1176	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ ze ) -> ch )
Theorem	simp311 1177	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ph )
Theorem	simp312 1178	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ps )
Theorem	simp313 1179	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ch )
Theorem	simp321 1180	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ph )
Theorem	simp322 1181	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ps )
Theorem	simp323 1182	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ch )
Theorem	simp331 1183	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ph )
Theorem	simp332 1184	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ps )
Theorem	simp333 1185	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ch )
Theorem	3adantl1 1186	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ta /\ ph /\ ps ) /\ ch ) -> th )
Theorem	3adantl2 1187	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ph /\ ta /\ ps ) /\ ch ) -> th )
Theorem	3adantl3 1188	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )
Theorem	3adantr1 1189	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ( ta /\ ps /\ ch ) ) -> th )
Theorem	3adantr2 1190	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta /\ ch ) ) -> th )
Theorem	3adantr3 1191	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )
Theorem	3ad2antl1 1192	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )
Theorem	3ad2antl2 1193	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ( ps /\ ph /\ ta ) /\ ch ) -> th )
Theorem	3ad2antl3 1194	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ( ps /\ ta /\ ph ) /\ ch ) -> th )
Theorem	3ad2antr1 1195	Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ph /\ ( ch /\ ps /\ ta ) ) -> th )
Theorem	3ad2antr2 1196	Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )
Theorem	3ad2antr3 1197	Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta /\ ch ) ) -> th )
Theorem	3anibar 1198	Remove a hypothesis from the second member of a biimplication. (Contributed by FL, 22-Jul-2008.)
|- ( ( ph /\ ps /\ ch ) -> ( th <-> ( ch /\ ta ) ) )   =>    |- ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) )
Theorem	3mix1 1199	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|- ( ph -> ( ph \/ ps \/ ch ) )
Theorem	3mix2 1200	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|- ( ph -> ( ps \/ ph \/ ch ) )