![]() |
Metamath
Proof Explorer Theorem List (p. 13 of 435) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28319) |
![]() (28320-29844) |
![]() (29845-43440) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3anbi2i 1201 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) ↔ (𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
Theorem | 3anbi3i 1202 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓)) | ||
Theorem | syl3an 1203 | A triple syllogism inference. (Contributed by NM, 13-May-2004.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜏 → 𝜂) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | syl3anb 1204 | A triple syllogism inference. (Contributed by NM, 15-Oct-2005.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜏 ↔ 𝜂) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | syl3anbr 1205 | A triple syllogism inference. (Contributed by NM, 29-Dec-2011.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜒) & ⊢ (𝜂 ↔ 𝜏) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | syl3an1 1206 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an2 1207 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.) |
⊢ (𝜑 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an2OLD 1208 | Obsolete version of syl3an2 1207 as of 26-Jun-2022. (Contributed by NM, 22-Aug-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an3 1209 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.) |
⊢ (𝜑 → 𝜃) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) | ||
Theorem | syl3an3OLD 1210 | Obsolete version of syl3an3 1209 as of 26-Jun-2022. (Contributed by NM, 22-Aug-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜃) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) | ||
Theorem | 3adantl1 1211 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adantl2 1212 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adantl3 1213 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adantr1 1214 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adantr2 1215 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adantr3 1216 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) | ||
Theorem | ad4ant123 1217 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜃) | ||
Theorem | ad4ant123OLD 1218 | Obsolete version of ad4ant123 1217 as of 14-Apr-2022. (Contributed by Alan Sare, 17-Oct-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜃) | ||
Theorem | ad4ant124 1219 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | ad4ant124OLD 1220 | Obsolete version of ad4ant124 1219 as of 14-Apr-2022. (Contributed by Alan Sare, 17-Oct-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | ad4ant134 1221 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | ad4ant134OLD 1222 | Obsolete version of ad4ant134 1221 as of 14-Apr-2022. (Contributed by Alan Sare, 17-Oct-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | ad4ant234 1223 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | ad4ant234OLD 1224 | Obsolete version of ad4ant234 1223 as of 14-Apr-2022. (Contributed by Alan Sare, 17-Oct-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant1l 1225 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant1lOLD 1226 | Obsolete version of 3adant1l 1225 as of 23-Jun-2022. (Contributed by NM, 8-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant1r 1227 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant1rOLD 1228 | Obsolete version of 3adant1r 1227 as of 23-Jun-2022. (Contributed by NM, 8-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant2l 1229 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant2lOLD 1230 | Obsolete version of 3adant2l 1229 as of 25-Jun-2022. (Contributed by NM, 8-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant2r 1231 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant2rOLD 1232 | Obsolete version of 3adant2r 1231 as of 25-Jun-2022. (Contributed by NM, 8-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant3l 1233 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adant3lOLD 1234 | Obsolete version of 3adant3l 1233 as of 25-Jun-2022. (Contributed by NM, 8-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adant3r 1235 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) | ||
Theorem | 3adant3rOLD 1236 | Obsolete version of 3adant3r 1235 as of 25-Jun-2022. (Contributed by NM, 8-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) | ||
Theorem | 3adant3r1 1237 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adant3r2 1238 | Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adant3r3 1239 | Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) | ||
Theorem | 3ad2antl1 1240 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3ad2antl2 1241 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3ad2antl3 1242 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃) | ||
Theorem | 3ad2antr1 1243 | Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) | ||
Theorem | 3ad2antr2 1244 | Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) | ||
Theorem | 3ad2antr3 1245 | Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | simpl1 1246 | Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) | ||
Theorem | simpl1OLD 1247 | Obsolete version of simpl1 1246 as of 23-Jun-2022. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) | ||
Theorem | simpl2 1248 | Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | ||
Theorem | simpl2OLD 1249 | Obsolete version of simpl2 1248 as of 23-Jun-2022. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | ||
Theorem | simpl3 1250 | Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) | ||
Theorem | simpl3OLD 1251 | Obsolete version of simpl3 1250 as of 23-Jun-2022. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) | ||
Theorem | simpr1 1252 | Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓) | ||
Theorem | simpr1OLD 1253 | Obsolete version of simpr1 1252 as of 23-Jun-2022. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓) | ||
Theorem | simpr2 1254 | Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒) | ||
Theorem | simpr2OLD 1255 | Obsolete version of simpr2 1254 as of 23-Jun-2022. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒) | ||
Theorem | simpr3 1256 | Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃) | ||
Theorem | simpr3OLD 1257 | Obsolete version of simpr3 1256 as of 23-Jun-2022. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃) | ||
Theorem | simp1l 1258 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) | ||
Theorem | simp1r 1259 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | ||
Theorem | simp2l 1260 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | ||
Theorem | simp2r 1261 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) | ||
Theorem | simp3l 1262 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒) | ||
Theorem | simp3r 1263 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃) | ||
Theorem | simp11 1264 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
Theorem | simp12 1265 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
Theorem | simp13 1266 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒) | ||
Theorem | simp21 1267 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simp22 1268 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒) | ||
Theorem | simp23 1269 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜃) | ||
Theorem | simp31 1270 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒) | ||
Theorem | simp32 1271 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃) | ||
Theorem | simp33 1272 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏) | ||
Theorem | simpll1 1273 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
Theorem | simpll1OLD 1274 | Obsolete version of simpll1 1273 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
Theorem | simpll2 1275 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simpll2OLD 1276 | Obsolete version of simpll2 1275 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simpll3 1277 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒) | ||
Theorem | simpll3OLD 1278 | Obsolete version of simpll3 1277 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒) | ||
Theorem | simplr1 1279 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) | ||
Theorem | simplr1OLD 1280 | Obsolete version of simplr1 1279 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) | ||
Theorem | simplr2 1281 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓) | ||
Theorem | simplr2OLD 1282 | Obsolete version of simplr2 1281 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓) | ||
Theorem | simplr3 1283 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒) | ||
Theorem | simplr3OLD 1284 | Obsolete version of simplr3 1283 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒) | ||
Theorem | simprl1 1285 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) | ||
Theorem | simprl1OLD 1286 | Obsolete version of simprl1 1285 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) | ||
Theorem | simprl2 1287 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) | ||
Theorem | simprl2OLD 1288 | Obsolete version of simprl2 1287 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) | ||
Theorem | simprl3 1289 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) | ||
Theorem | simprl3OLD 1290 | Obsolete version of simprl3 1289 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) | ||
Theorem | simprr1 1291 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
Theorem | simprr1OLD 1292 | Obsolete version of simprr1 1291 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
Theorem | simprr2 1293 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
Theorem | simprr2OLD 1294 | Obsolete version of simprr2 1293 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
Theorem | simprr3 1295 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
Theorem | simprr3OLD 1296 | Obsolete version of simprr3 1295 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
Theorem | simpl1l 1297 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
Theorem | simpl1lOLD 1298 | Obsolete version of simpl1l 1297 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
Theorem | simpl1r 1299 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simpl1rOLD 1300 | Obsolete version of simpl1r 1299 as of 23-Jun-2022. (Contributed by NM, 9-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |