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	con3ALT 1101	Proof of con3 154 from its associated inference con3i 155 that illustrates the use of the weak deduction theorem dedt 1100. (Contributed by NM, 27-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) Revised dedt 1100 and elimh 1099. (Revised by Steven Nguyen, 27-Apr-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
1.2.11  Abbreviated conjunction and disjunction of three wff's
Syntax	w3o 1102	Extend wff definition to include three-way disjunction ('or').
wff (𝜑 ∨ 𝜓 ∨ 𝜒)
Syntax	w3a 1103	Extend wff definition to include three-way conjunction ('and').
wff (𝜑 ∧ 𝜓 ∧ 𝜒)
Definition	df-3or 1104	Define disjunction ('or') of three wff's. Definition *2.33 of [WhiteheadRussell] p. 105. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law orass 935. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
Definition	df-3an 1105	Define conjunction ('and') of three wff's. Definition *4.34 of [WhiteheadRussell] p. 118. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law anass 474. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
Theorem	3orass 1106	Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
Theorem	3orel1 1107	Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.)
⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜓 ∨ 𝜒)))
Theorem	3orrot 1108	Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))
Theorem	3orcoma 1109	Commutation law for triple disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜑 ∨ 𝜒))
Theorem	3orcomb 1110	Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.) (Proof shortened by Wolf Lammen, 8-Apr-2022.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓))
Theorem	3anass 1111	Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
Theorem	3anan12 1112	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 1115 by Wolf Lammen, 5-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒)))
Theorem	3anan32 1113	Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Shortened by Garrett Katz, 15-Jun-2026.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	3anan32OLD 1114	Obsolete version of 3anan32 1113 as of 15-Jun-2026. Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓))
Theorem	3ancoma 1115	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 5-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
Theorem	3ancomb 1116	Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Revised to shorten 3anrot 1117 by Wolf Lammen, 9-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓))
Theorem	3anrot 1117	Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.) (Proof shortened by Wolf Lammen, 9-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
Theorem	3anrev 1118	Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓 ∧ 𝜑))
Theorem	anandi3 1119	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)))
Theorem	anandi3r 1120	Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓)))
Theorem	3anidm 1121	Idempotent law for conjunction. (Contributed by Peter Mazsa, 17-Oct-2023.)
⊢ ((𝜑 ∧ 𝜑 ∧ 𝜑) ↔ 𝜑)
Theorem	3an4anass 1122	Associative law for four conjunctions with a triple conjunction. (Contributed by Alexander van der Vekens, 24-Jun-2018.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
Theorem	3ioran 1123	Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)
⊢ (¬ (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒))
Theorem	3ianor 1124	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 336. (Revised by Wolf Lammen, 8-Apr-2022.)
⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒))
Theorem	3anor 1125	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 1126	Triple disjunction in terms of triple conjunction. (Contributed by NM, 8-Oct-2012.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ¬ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒))
Theorem	3impa 1127	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3imp 1128 by Wolf Lammen, 20-Jun-2022.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3imp 1128	Importation inference. (Contributed by NM, 8-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jun-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3imp31 1129	The importation inference 3imp 1128 with commutation of the first and third conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)
Theorem	3imp231 1130	Importation inference. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)
Theorem	3imp21 1131	The importation inference 3imp 1128 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 1141 by Wolf Lammen, 23-Jun-2022.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
Theorem	3impb 1132	Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi23imp13 1133	3imp 1128 with middle implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3impib 1134	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3impia 1135	Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3expa 1136	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3exp 1137 and pm3.2an3 1359 by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3exp 1137	Exportation inference. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	3expb 1138	Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
Theorem	3expia 1139	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
Theorem	3expib 1140	Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
Theorem	3com12 1141	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 1142	Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)
Theorem	3comr 1143	Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.) Theorems shortened and reordered. (Revised by Wolf Lammen, 9-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)
Theorem	3com23 1144	Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 9-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)
Theorem	3coml 1145	Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)
Theorem	3jca 1146	Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	3jcad 1147	Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏)))
Theorem	3adant1 1148	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒)
Theorem	3adant2 1149	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒)
Theorem	3adant3 1150	Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)
Theorem	3ad2ant1 1151	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)
Theorem	3ad2ant2 1152	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒)
Theorem	3ad2ant3 1153	Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒)
Theorem	simp1 1154	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
Theorem	simp2 1155	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
Theorem	simp3 1156	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
Theorem	simp1i 1157	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)    ⇒   ⊢ 𝜑
Theorem	simp2i 1158	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)    ⇒   ⊢ 𝜓
Theorem	simp3i 1159	Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒)    ⇒   ⊢ 𝜒
Theorem	simp1d 1160	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	simp2d 1161	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simp3d 1162	Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	simp1bi 1163	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	simp2bi 1164	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	simp3bi 1165	Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	3simpa 1166	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))
Theorem	3simpb 1167	Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒))
Theorem	3simpc 1168	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 1169	Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜏 → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))
Theorem	3anim1i 1170	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	3anim2i 1171	Add two conjuncts to antecedent and consequent. (Contributed by AV, 21-Nov-2019.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	3anim3i 1172	Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓))
Theorem	3anbi123i 1173	Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜏 ↔ 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂))
Theorem	3orbi123i 1174	Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜏 ↔ 𝜂)    ⇒   ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))
Theorem	3anbi1i 1175	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
Theorem	3anbi2i 1176	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) ↔ (𝜒 ∧ 𝜓 ∧ 𝜃))
Theorem	3anbi3i 1177	Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓))
Theorem	syl3an 1178	A triple syllogism inference. (Contributed by NM, 13-May-2004.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜏 → 𝜂)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	syl3anb 1179	A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜏 ↔ 𝜂)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	syl3anbr 1180	A triple syllogism inference. (Contributed by NM, 29-Dec-2011.)
⊢ (𝜓 ↔ 𝜑)    &   ⊢ (𝜃 ↔ 𝜒)    &   ⊢ (𝜂 ↔ 𝜏)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	syl3an1 1181	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)
Theorem	syl3an2 1182	A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)
⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏)
Theorem	syl3an3 1183	A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)
⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏)
Theorem	syl3an132 1184	syl2an 608 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂)
Theorem	3adantl1 1185	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3adantl2 1186	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3adantl3 1187	Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	3adantr1 1188	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)
Theorem	3adantr2 1189	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃)
Theorem	3adantr3 1190	Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)
Theorem	ad4ant123 1191	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜃)
Theorem	ad4ant124 1192	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	ad4ant134 1193	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	ad4ant234 1194	Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3adant1l 1195	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3adant1r 1196	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	3adant2l 1197	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)
Theorem	3adant2r 1198	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)
Theorem	3adant3l 1199	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)
Theorem	3adant3r 1200	Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)