P. 12 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1101-1200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	simp2r1 1101	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ph )
Theorem	simp2r2 1102	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ps )
Theorem	simp2r3 1103	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( th /\ ( ph /\ ps /\ ch ) ) /\ et ) -> ch )
Theorem	simp3l1 1104	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ph )
Theorem	simp3l2 1105	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ps )
Theorem	simp3l3 1106	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ( ph /\ ps /\ ch ) /\ th ) ) -> ch )
Theorem	simp3r1 1107	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ph )
Theorem	simp3r2 1108	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ps )
Theorem	simp3r3 1109	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( th /\ ( ph /\ ps /\ ch ) ) ) -> ch )
Theorem	simp11l 1110	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta /\ et ) -> ph )
Theorem	simp11r 1111	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps ) /\ ch /\ th ) /\ ta /\ et ) -> ps )
Theorem	simp12l 1112	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta /\ et ) -> ph )
Theorem	simp12r 1113	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ ( ph /\ ps ) /\ th ) /\ ta /\ et ) -> ps )
Theorem	simp13l 1114	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta /\ et ) -> ph )
Theorem	simp13r 1115	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ch /\ th /\ ( ph /\ ps ) ) /\ ta /\ et ) -> ps )
Theorem	simp21l 1116	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps ) /\ ch /\ th ) /\ et ) -> ph )
Theorem	simp21r 1117	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ( ph /\ ps ) /\ ch /\ th ) /\ et ) -> ps )
Theorem	simp22l 1118	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ ( ph /\ ps ) /\ th ) /\ et ) -> ph )
Theorem	simp22r 1119	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ ( ph /\ ps ) /\ th ) /\ et ) -> ps )
Theorem	simp23l 1120	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ th /\ ( ph /\ ps ) ) /\ et ) -> ph )
Theorem	simp23r 1121	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ ( ch /\ th /\ ( ph /\ ps ) ) /\ et ) -> ps )
Theorem	simp31l 1122	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ( ph /\ ps ) /\ ch /\ th ) ) -> ph )
Theorem	simp31r 1123	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ( ph /\ ps ) /\ ch /\ th ) ) -> ps )
Theorem	simp32l 1124	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ch /\ ( ph /\ ps ) /\ th ) ) -> ph )
Theorem	simp32r 1125	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ch /\ ( ph /\ ps ) /\ th ) ) -> ps )
Theorem	simp33l 1126	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ch /\ th /\ ( ph /\ ps ) ) ) -> ph )
Theorem	simp33r 1127	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ta /\ et /\ ( ch /\ th /\ ( ph /\ ps ) ) ) -> ps )
Theorem	simp111 1128	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et /\ ze ) -> ph )
Theorem	simp112 1129	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et /\ ze ) -> ps )
Theorem	simp113 1130	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ et /\ ze ) -> ch )
Theorem	simp121 1131	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et /\ ze ) -> ph )
Theorem	simp122 1132	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et /\ ze ) -> ps )
Theorem	simp123 1133	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ et /\ ze ) -> ch )
Theorem	simp131 1134	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et /\ ze ) -> ph )
Theorem	simp132 1135	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et /\ ze ) -> ps )
Theorem	simp133 1136	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ et /\ ze ) -> ch )
Theorem	simp211 1137	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ ze ) -> ph )
Theorem	simp212 1138	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ ze ) -> ps )
Theorem	simp213 1139	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) /\ ze ) -> ch )
Theorem	simp221 1140	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ ze ) -> ph )
Theorem	simp222 1141	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ ze ) -> ps )
Theorem	simp223 1142	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) /\ ze ) -> ch )
Theorem	simp231 1143	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ ze ) -> ph )
Theorem	simp232 1144	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ ze ) -> ps )
Theorem	simp233 1145	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) /\ ze ) -> ch )
Theorem	simp311 1146	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ph )
Theorem	simp312 1147	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ps )
Theorem	simp313 1148	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( ( ph /\ ps /\ ch ) /\ th /\ ta ) ) -> ch )
Theorem	simp321 1149	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ph )
Theorem	simp322 1150	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ps )
Theorem	simp323 1151	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ( ph /\ ps /\ ch ) /\ ta ) ) -> ch )
Theorem	simp331 1152	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ph )
Theorem	simp332 1153	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ps )
Theorem	simp333 1154	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|- ( ( et /\ ze /\ ( th /\ ta /\ ( ph /\ ps /\ ch ) ) ) -> ch )
Theorem	3adantl1 1155	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ta /\ ph /\ ps ) /\ ch ) -> th )
Theorem	3adantl2 1156	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ph /\ ta /\ ps ) /\ ch ) -> th )
Theorem	3adantl3 1157	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )
Theorem	3adantr1 1158	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ( ta /\ ps /\ ch ) ) -> th )
Theorem	3adantr2 1159	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta /\ ch ) ) -> th )
Theorem	3adantr3 1160	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )
Theorem	3ad2antl1 1161	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ( ph /\ ps /\ ta ) /\ ch ) -> th )
Theorem	3ad2antl2 1162	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ( ps /\ ph /\ ta ) /\ ch ) -> th )
Theorem	3ad2antl3 1163	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ( ps /\ ta /\ ph ) /\ ch ) -> th )
Theorem	3ad2antr1 1164	Deduction adding a conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ph /\ ( ch /\ ps /\ ta ) ) -> th )
Theorem	3ad2antr2 1165	Deduction adding a conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ch /\ ta ) ) -> th )
Theorem	3ad2antr3 1166	Deduction adding a conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.)
|- ( ( ph /\ ch ) -> th )   =>    |- ( ( ph /\ ( ps /\ ta /\ ch ) ) -> th )
Theorem	3anibar 1167	Remove a hypothesis from the second member of a biconditional. (Contributed by FL, 22-Jul-2008.)
|- ( ( ph /\ ps /\ ch ) -> ( th <-> ( ch /\ ta ) ) )   =>    |- ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) )
Theorem	3mix1 1168	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|- ( ph -> ( ph \/ ps \/ ch ) )
Theorem	3mix2 1169	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|- ( ph -> ( ps \/ ph \/ ch ) )
Theorem	3mix3 1170	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|- ( ph -> ( ps \/ ch \/ ph ) )
Theorem	3mix1i 1171	Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.)
|- ph   =>    |- ( ph \/ ps \/ ch )
Theorem	3mix2i 1172	Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.)
|- ph   =>    |- ( ps \/ ph \/ ch )
Theorem	3mix3i 1173	Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.)
|- ph   =>    |- ( ps \/ ch \/ ph )
Theorem	3mix1d 1174	Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)
|- ( ph -> ps )   =>    |- ( ph -> ( ps \/ ch \/ th ) )
Theorem	3mix2d 1175	Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)
|- ( ph -> ps )   =>    |- ( ph -> ( ch \/ ps \/ th ) )
Theorem	3mix3d 1176	Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)
|- ( ph -> ps )   =>    |- ( ph -> ( ch \/ th \/ ps ) )
Theorem	3pm3.2i 1177	Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)
|- ph   &    |- ps   &    |- ch   =>    |- ( ph /\ ps /\ ch )
Theorem	pm3.2an3 1178	pm3.2 139 for a triple conjunction. (Contributed by Alan Sare, 24-Oct-2011.)
|- ( ph -> ( ps -> ( ch -> ( ph /\ ps /\ ch ) ) ) )
Theorem	3jca 1179	Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   =>    |- ( ph -> ( ps /\ ch /\ th ) )
Theorem	3jcad 1180	Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> th ) )   &    |- ( ph -> ( ps -> ta ) )   =>    |- ( ph -> ( ps -> ( ch /\ th /\ ta ) ) )
Theorem	mpbir3an 1181	Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 9-Jan-2015.)
|- ps   &    |- ch   &    |- th   &    |- ( ph <-> ( ps /\ ch /\ th ) )   =>    |- ph
Theorem	mpbir3and 1182	Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.)
|- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> ( ps <-> ( ch /\ th /\ ta ) ) )   =>    |- ( ph -> ps )
Theorem	syl3anbrc 1183	Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ta <-> ( ps /\ ch /\ th ) )   =>    |- ( ph -> ta )
Theorem	syl21anbrc 1184	Syllogism inference. (Contributed by Peter Mazsa, 18-Sep-2022.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ta <-> ( ( ps /\ ch ) /\ th ) )   =>    |- ( ph -> ta )
Theorem	3imp3i2an 1185	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 13-Apr-2022.)
|- ( ( ph /\ ps /\ ch ) -> th )   &    |- ( ( ph /\ ch ) -> ta )   &    |- ( ( th /\ ta ) -> et )   =>    |- ( ( ph /\ ps /\ ch ) -> et )
Theorem	3anim123i 1186	Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)
|- ( ph -> ps )   &    |- ( ch -> th )   &    |- ( ta -> et )   =>    |- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )
Theorem	3anim1i 1187	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)
|- ( ph -> ps )   =>    |- ( ( ph /\ ch /\ th ) -> ( ps /\ ch /\ th ) )
Theorem	3anim2i 1188	Add two conjuncts to antecedent and consequent. (Contributed by AV, 21-Nov-2019.)
|- ( ph -> ps )   =>    |- ( ( ch /\ ph /\ th ) -> ( ch /\ ps /\ th ) )
Theorem	3anim3i 1189	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)
|- ( ph -> ps )   =>    |- ( ( ch /\ th /\ ph ) -> ( ch /\ th /\ ps ) )
Theorem	3anbi123i 1190	Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   &    |- ( ta <-> et )   =>    |- ( ( ph /\ ch /\ ta ) <-> ( ps /\ th /\ et ) )
Theorem	3orbi123i 1191	Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   &    |- ( ta <-> et )   =>    |- ( ( ph \/ ch \/ ta ) <-> ( ps \/ th \/ et ) )
Theorem	3anbi1i 1192	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
|- ( ph <-> ps )   =>    |- ( ( ph /\ ch /\ th ) <-> ( ps /\ ch /\ th ) )
Theorem	3anbi2i 1193	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
|- ( ph <-> ps )   =>    |- ( ( ch /\ ph /\ th ) <-> ( ch /\ ps /\ th ) )
Theorem	3anbi3i 1194	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
|- ( ph <-> ps )   =>    |- ( ( ch /\ th /\ ph ) <-> ( ch /\ th /\ ps ) )
Theorem	3imp 1195	Importation inference. (Contributed by NM, 8-Apr-1994.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3impa 1196	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ch ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	ex3 1197	Apply ex 115 to a hypothesis with a 3-right-nested conjunction antecedent, with the antecedent of the assertion being a triple conjunction rather than a 2-right-nested conjunction. (Contributed by Alan Sare, 22-Apr-2018.)
|- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )   =>    |- ( ( ph /\ ps /\ ch ) -> ( th -> ta ) )
Theorem	3imp31 1198	The importation inference 3imp 1195 with commutation of the first and third conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ( ch /\ ps /\ ph ) -> th )
Theorem	3imp231 1199	Importation inference. (Contributed by Alan Sare, 17-Oct-2017.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ( ps /\ ch /\ ph ) -> th )
Theorem	3imp21 1200	The importation inference 3imp 1195 with commutation of the first and second conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.) (Revised to shorten 3com12 1209 by Wolf Lammen, 23-Jun-2022.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ( ps /\ ph /\ ch ) -> th )