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