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	3anan12 1101	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised to shorten 3ancoma 1103 by Wolf Lammen, 5-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
Theorem	3anan32 1102	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	3ancoma 1103	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 5-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
Theorem	3ancomb 1104	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Revised to shorten 3anrot 1105 by Wolf Lammen, 9-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))
Theorem	3anrot 1105	Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.) (Proof shortened by Wolf Lammen, 9-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
Theorem	3anrev 1106	Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓 ∧ 𝜑))
Theorem	anandi3 1107	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
Theorem	anandi3r 1108	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓)))
Theorem	3anidm 1109	Idempotent law for conjunction. (Contributed by Peter Mazsa, 17-Oct-2023.)
⊢ ((𝜑 ∧ 𝜑 ∧ 𝜑) ↔ 𝜑)
Theorem	3an4anass 1110	Associative law for four conjunctions with a triple conjunction. (Contributed by Alexander van der Vekens, 24-Jun-2018.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
Theorem	3ioran 1111	Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)
⊢ (¬ (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒))
Theorem	3ianor 1112	Negated triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) Shorten with xchnxbir 334. (Revised by Wolf Lammen, 8-Apr-2022.)
⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))
Theorem	3anor 1113	Triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Wolf Lammen, 8-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))
Theorem	3oran 1114	Triple disjunction in terms of triple conjunction. (Contributed by NM, 8-Oct-2012.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ¬ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒))
Theorem	3impa 1115	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3imp 1116 by Wolf Lammen, 20-Jun-2022.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3imp 1116	Importation inference. (Contributed by NM, 8-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jun-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3imp31 1117	The importation inference 3imp 1116 with commutation of the first and third conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)
Theorem	3imp231 1118	Importation inference. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)
Theorem	3imp21 1119	The importation inference 3imp 1116 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 1129 by Wolf Lammen, 23-Jun-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
Theorem	3impb 1120	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi23imp13 1121	3imp 1116 with middle implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3impib 1122	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3impia 1123	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3expa 1124	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3exp 1125 and pm3.2an3 1347 by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3exp 1125	Exportation inference. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	3expb 1126	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
Theorem	3expia 1127	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
Theorem	3expib 1128	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	3com12 1129	Commutation in antecedent. Swap 1st and 2nd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
Theorem	3com13 1130	Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)
Theorem	3comr 1131	Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.) Theorems shortened and reordered. (Revised by Wolf Lammen, 9-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)
Theorem	3com23 1132	Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 9-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)
Theorem	3coml 1133	Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)
Theorem	3jca 1134	Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	3jcad 1135	Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏)))
Theorem	3adant1 1136	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)
Theorem	3adant2 1137	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒)
Theorem	3adant3 1138	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)
Theorem	3ad2ant1 1139	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)
Theorem	3ad2ant2 1140	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒)
Theorem	3ad2ant3 1141	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)
Theorem	simp1 1142	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
Theorem	simp2 1143	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
Theorem	simp3 1144	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
Theorem	simp1i 1145	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)    ⇒   ⊢ 𝜑
Theorem	simp2i 1146	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)    ⇒   ⊢ 𝜓
Theorem	simp3i 1147	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)    ⇒   ⊢ 𝜒
Theorem	simp1d 1148	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	simp2d 1149	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simp3d 1150	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	simp1bi 1151	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	simp2bi 1152	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simp3bi 1153	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	3simpa 1154	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))
Theorem	3simpb 1155	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))
Theorem	3simpc 1156	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
Theorem	3anim123i 1157	Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜏 → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))
Theorem	3anim1i 1158	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	3anim2i 1159	Add two conjuncts to antecedent and consequent. (Contributed by AV, 21-Nov-2019.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	3anim3i 1160	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓))
Theorem	3anbi123i 1161	Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜏 ↔ 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂))
Theorem	3orbi123i 1162	Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜏 ↔ 𝜂)    ⇒   ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))
Theorem	3anbi1i 1163	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	3anbi2i 1164	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) ↔ (𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	3anbi3i 1165	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓))
Theorem	syl3an 1166	A triple syllogism inference. (Contributed by NM, 13-May-2004.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜏 → 𝜂)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	syl3anb 1167	A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜏 ↔ 𝜂)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	syl3anbr 1168	A triple syllogism inference. (Contributed by NM, 29-Dec-2011.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜒)    &   ⊢ (𝜂 ↔ 𝜏)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	syl3an1 1169	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2 1170	A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)
⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3 1171	A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)
⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syl3an132 1172	syl2an 602 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂)
Theorem	3adantl1 1173	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3adantl2 1174	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3adantl3 1175	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	3adantr1 1176	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)
Theorem	3adantr2 1177	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)
Theorem	3adantr3 1178	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)
Theorem	ad4ant123 1179	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜃)
Theorem	ad4ant124 1180	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	ad4ant134 1181	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	ad4ant234 1182	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3adant1l 1183	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3adant1r 1184	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3adant2l 1185	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3adant2r 1186	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	3adant3l 1187	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)
Theorem	3adant3r 1188	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)
Theorem	3adant3r1 1189	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)
Theorem	3adant3r2 1190	Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)
Theorem	3adant3r3 1191	Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)
Theorem	3ad2antl1 1192	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	3ad2antl2 1193	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	3ad2antl3 1194	Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃)
Theorem	3ad2antr1 1195	Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)
⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃)
Theorem	3ad2antr2 1196	Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)
⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)
Theorem	3ad2antr3 1197	Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.)
⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)
Theorem	simpl1 1198	Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)
Theorem	simpl2 1199	Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)
Theorem	simpl3 1200	Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)