P. 13 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1201-1300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3jca 1201	Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	3jcad 1202	Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏)))
Theorem	mpbir3an 1203	Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 9-Jan-2015.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ 𝜑
Theorem	mpbir3and 1204	Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	syl3anbrc 1205	Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl21anbrc 1206	Syllogism inference. (Contributed by Peter Mazsa, 18-Sep-2022.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜏 ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	3imp3i2an 1207	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 13-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜏)    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜂)
Theorem	3anim123i 1208	Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜏 → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))
Theorem	3anim1i 1209	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	3anim2i 1210	Add two conjuncts to antecedent and consequent. (Contributed by AV, 21-Nov-2019.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	3anim3i 1211	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓))
Theorem	3anbi123i 1212	Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜏 ↔ 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂))
Theorem	3orbi123i 1213	Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜏 ↔ 𝜂)    ⇒   ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))
Theorem	3anbi1i 1214	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	3anbi2i 1215	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) ↔ (𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	3anbi3i 1216	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓))
Theorem	3imp 1217	Importation inference. (Contributed by NM, 8-Apr-1994.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3impa 1218	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	ex3 1219	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.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏))
Theorem	3imp31 1220	The importation inference 3imp 1217 with commutation of the first and third conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)
Theorem	3imp231 1221	Importation inference. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)
Theorem	3imp21 1222	The importation inference 3imp 1217 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 1231 by Wolf Lammen, 23-Jun-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
Theorem	3impb 1223	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3impia 1224	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3impib 1225	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3exp 1226	Exportation inference. (Contributed by NM, 30-May-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	3expa 1227	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3expb 1228	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
Theorem	3expia 1229	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
Theorem	3expib 1230	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	3com12 1231	Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
Theorem	3com13 1232	Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)
Theorem	3com23 1233	Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)
Theorem	3coml 1234	Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)
Theorem	3comr 1235	Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)
Theorem	3adant3r1 1236	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)
Theorem	3adant3r2 1237	Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)
Theorem	3adant3r3 1238	Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)
Theorem	ad4ant123 1239	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜃)
Theorem	ad4ant124 1240	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	ad4ant134 1241	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	ad4ant234 1242	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3an1rs 1243	Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒) → 𝜏)
Theorem	3imp1 1244	Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	3impd 1245	Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
Theorem	3imp2 1246	Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)
Theorem	3exp1 1247	Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	3expd 1248	Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	3exp2 1249	Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp5o 1250	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp516 1251	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp520 1252	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	3anassrs 1253	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	3adant1l 1254	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3adant1r 1255	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3adant2l 1256	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3adant2r 1257	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	3adant3l 1258	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)
Theorem	3adant3r 1259	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)
Theorem	ad5ant245 1260	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜏 ∧ 𝜑) ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	ad5ant234 1261	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) ∧ 𝜂) → 𝜃)
Theorem	ad5ant235 1262	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜂) ∧ 𝜒) → 𝜃)
Theorem	ad5ant123 1263	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜃)
Theorem	ad5ant124 1264	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) ∧ 𝜂) → 𝜃)
Theorem	ad5ant125 1265	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜂) ∧ 𝜒) → 𝜃)
Theorem	ad5ant134 1266	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) ∧ 𝜂) → 𝜃)
Theorem	ad5ant135 1267	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) ∧ 𝜒) → 𝜃)
Theorem	ad5ant145 1268	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	syl12anc 1269	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl21anc 1270	Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl3anc 1271	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl22anc 1272	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl13anc 1273	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl31anc 1274	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl112anc 1275	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl121anc 1276	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl211anc 1277	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl23anc 1278	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl32anc 1279	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl122anc 1280	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl212anc 1281	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl221anc 1282	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl113anc 1283	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl131anc 1284	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl311anc 1285	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	syl33anc 1286	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl222anc 1287	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl123anc 1288	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl132anc 1289	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl213anc 1290	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl231anc 1291	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl312anc 1292	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁)) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl321anc 1293	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)    ⇒   ⊢ (𝜑 → 𝜎)
Theorem	syl133anc 1294	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl313anc 1295	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl331anc 1296	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl223anc 1297	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl232anc 1298	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl322anc 1299	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌)    ⇒   ⊢ (𝜑 → 𝜌)
Theorem	syl233anc 1300	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (𝜑 → 𝜁)    &   ⊢ (𝜑 → 𝜎)    &   ⊢ (𝜑 → 𝜌)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇)    ⇒   ⊢ (𝜑 → 𝜇)