P. 14 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 1301-1400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	simp11l 1301	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)
Theorem	simp11r 1302	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓)
Theorem	simp12l 1303	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑)
Theorem	simp12r 1304	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓)
Theorem	simp13l 1305	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜑)
Theorem	simp13r 1306	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓)
Theorem	simp21l 1307	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜑)
Theorem	simp21r 1308	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜓)
Theorem	simp22l 1309	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑)
Theorem	simp22r 1310	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓)
Theorem	simp23l 1311	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑)
Theorem	simp23r 1312	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓)
Theorem	simp31l 1313	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑)
Theorem	simp31r 1314	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)
Theorem	simp32l 1315	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑)
Theorem	simp32r 1316	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓)
Theorem	simp33l 1317	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑)
Theorem	simp33r 1318	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓)
Theorem	simp111 1319	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑)
Theorem	simp112 1320	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓)
Theorem	simp113 1321	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒)
Theorem	simp121 1322	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑)
Theorem	simp122 1323	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓)
Theorem	simp123 1324	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒)
Theorem	simp131 1325	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑)
Theorem	simp132 1326	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜓)
Theorem	simp133 1327	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒)
Theorem	simp211 1328	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜑)
Theorem	simp212 1329	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜓)
Theorem	simp213 1330	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜒)
Theorem	simp221 1331	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜑)
Theorem	simp222 1332	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜓)
Theorem	simp223 1333	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜒)
Theorem	simp231 1334	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜑)
Theorem	simp232 1335	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜓)
Theorem	simp233 1336	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜒)
Theorem	simp311 1337	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ 𝜁 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜑)
Theorem	simp312 1338	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ 𝜁 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜓)
Theorem	simp313 1339	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ 𝜁 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜒)
Theorem	simp321 1340	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜑)
Theorem	simp322 1341	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜓)
Theorem	simp323 1342	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜒)
Theorem	simp331 1343	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑)
Theorem	simp332 1344	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓)
Theorem	simp333 1345	Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒)
Theorem	3anibar 1346	Remove a hypothesis from the second member of a biconditional. (Contributed by FL, 22-Jul-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ (𝜒 ∧ 𝜏)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))
Theorem	3mix1 1347	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒))
Theorem	3mix2 1348	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
⊢ (𝜑 → (𝜓 ∨ 𝜑 ∨ 𝜒))
Theorem	3mix3 1349	Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑))
Theorem	3mix1i 1350	Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.)
⊢ 𝜑    ⇒   ⊢ (𝜑 ∨ 𝜓 ∨ 𝜒)
Theorem	3mix2i 1351	Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ∨ 𝜑 ∨ 𝜒)
Theorem	3mix3i 1352	Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ∨ 𝜒 ∨ 𝜑)
Theorem	3mix1d 1353	Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃))
Theorem	3mix2d 1354	Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃))
Theorem	3mix3d 1355	Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓))
Theorem	3pm3.2i 1356	Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    ⇒   ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)
Theorem	pm3.2an3 1357	Version of pm3.2 474 for a triple conjunction. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by Kyle Wyonch, 24-Apr-2021.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 ∧ 𝜓 ∧ 𝜒))))
Theorem	mpbir3an 1358	Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.)
⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ 𝜑
Theorem	mpbir3and 1359	Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.) (Revised by Mario Carneiro, 9-Jan-2015.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	syl3anbrc 1360	Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl21anbrc 1361	Syllogism inference. (Contributed by Peter Mazsa, 18-Sep-2022.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜏 ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	3imp3i2an 1362	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 13-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜏)    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜂)
Theorem	ex3 1363	Apply ex 417 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	3imp1 1364	Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	3impd 1365	Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))
Theorem	3imp2 1366	Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)
Theorem	3impdi 1367	Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3impdir 1368	Importation inference (undistribute conjunction). (Contributed by NM, 20-Aug-1995.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)
Theorem	3exp1 1369	Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	3expd 1370	Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	3exp2 1371	Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
Theorem	exp5o 1372	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp516 1373	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	exp520 1374	A triple exportation inference. (Contributed by Jeff Hankins, 8-Jul-2009.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂)))))
Theorem	3impexp 1375	Version of impexp 455 for a triple conjunction. (Contributed by Alan Sare, 31-Dec-2011.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃))))
Theorem	3an1rs 1376	Swap conjuncts. (Contributed by NM, 16-Dec-2007.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒) → 𝜏)
Theorem	3anassrs 1377	Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	4anpull2 1378	An equivalence of two four-terms conjunctions with the terms regrouped (here, the second sub-conjunct of the first term is pulled separately). (Contributed by Zhi Wang, 4-Sep-2024.) (Proof shortened by Garrett Katz, 26-Jun-2026.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓))
Theorem	4anpull2OLD 1379	Obsolete version of 4anpull2 1378 as of 26-Jun-2026. An equivalence of two four-terms conjunctions with the terms regrouped (here, the second sub-conjunct of the first term is pulled separately). (Contributed by Zhi Wang, 4-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜓))
Theorem	ad5ant245 1380	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜏 ∧ 𝜑) ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	ad5ant234 1381	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) ∧ 𝜂) → 𝜃)
Theorem	ad5ant235 1382	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜂) ∧ 𝜒) → 𝜃)
Theorem	ad5ant123 1383	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜃)
Theorem	ad5ant124 1384	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) (Proof shortened by Garrett Katz, 13-Jun-2026.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) ∧ 𝜂) → 𝜃)
Theorem	ad5ant124OLD 1385	Obsolete version of ad5ant124 1384 as of 13-Jun-2026. Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) ∧ 𝜂) → 𝜃)
Theorem	ad5ant125 1386	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) (Proof shortened by Garrett Katz, 13-Jun-2026.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜂) ∧ 𝜒) → 𝜃)
Theorem	ad5ant125OLD 1387	Obsolete version of ad5ant125 1386 as of 13-Jun-2026. Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜂) ∧ 𝜒) → 𝜃)
Theorem	ad5ant134 1388	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) (Proof shortened by Garrett Katz, 13-Jun-2026.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) ∧ 𝜂) → 𝜃)
Theorem	ad5ant134OLD 1389	Obsolete version of ad5ant134 1388 as of 13-Jun-2026. Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) ∧ 𝜂) → 𝜃)
Theorem	ad5ant135 1390	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) (Proof shortened by Garrett Katz, 13-Jun-2026.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) ∧ 𝜒) → 𝜃)
Theorem	ad5ant135OLD 1391	Obsolete version of ad5ant135 1390 as of 13-Jun-2026. Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) ∧ 𝜒) → 𝜃)
Theorem	ad5ant145 1392	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	ad5ant2345 1393	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ (((((𝜂 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	syl3anc 1394	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	syl13anc 1395	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl31anc 1396	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl112anc 1397	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl121anc 1398	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl211anc 1399	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	syl23anc 1400	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)