HomeTheorem List (p. 13 of 429)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 13 of 429) | < 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: | Metamath Proof Explorer
(1-27903) |
Hilbert Space Explorer
(27904-29428) |
Users' Mathboxes
(29429-42879) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | simp22r 1201 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓) | ||
| Theorem | simp23l 1202 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑) | ||
| Theorem | simp23r 1203 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓) | ||
| Theorem | simp31l 1204 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) | ||
| Theorem | simp31r 1205 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) | ||
| Theorem | simp32l 1206 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) | ||
| Theorem | simp32r 1207 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) | ||
| Theorem | simp33l 1208 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) | ||
| Theorem | simp33r 1209 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) | ||
| Theorem | simp111 1210 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑) | ||
| Theorem | simp112 1211 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓) | ||
| Theorem | simp113 1212 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒) | ||
| Theorem | simp121 1213 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑) | ||
| Theorem | simp122 1214 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓) | ||
| Theorem | simp123 1215 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒) | ||
| Theorem | simp131 1216 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑) | ||
| Theorem | simp132 1217 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜓) | ||
| Theorem | simp133 1218 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒) | ||
| Theorem | simp211 1219 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜑) | ||
| Theorem | simp212 1220 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜓) | ||
| Theorem | simp213 1221 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜒) | ||
| Theorem | simp221 1222 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜑) | ||
| Theorem | simp222 1223 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜓) | ||
| Theorem | simp223 1224 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜒) | ||
| Theorem | simp231 1225 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜑) | ||
| Theorem | simp232 1226 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜓) | ||
| Theorem | simp233 1227 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜒) | ||
| Theorem | simp311 1228 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜑) | ||
| Theorem | simp312 1229 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜓) | ||
| Theorem | simp313 1230 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜒) | ||
| Theorem | simp321 1231 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜑) | ||
| Theorem | simp322 1232 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜓) | ||
| Theorem | simp323 1233 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜒) | ||
| Theorem | simp331 1234 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
| Theorem | simp332 1235 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
| Theorem | simp333 1236 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
| Theorem | 3adantl1 1237 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
| Theorem | 3adantl2 1238 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
| Theorem | 3adantl3 1239 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
| Theorem | 3adantr1 1240 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) | ||
| Theorem | 3adantr2 1241 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) | ||
| Theorem | 3adantr3 1242 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) | ||
| Theorem | 3ad2antl1 1243 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
| ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
| Theorem | 3ad2antl2 1244 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
| ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
| Theorem | 3ad2antl3 1245 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
| ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃) | ||
| Theorem | 3ad2antr1 1246 | Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.) |
| ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) | ||
| Theorem | 3ad2antr2 1247 | Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.) |
| ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) | ||
| Theorem | 3ad2antr3 1248 | Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.) |
| ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) | ||
| Theorem | 3anibar 1249 | Remove a hypothesis from the second member of a biimplication. (Contributed by FL, 22-Jul-2008.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ (𝜒 ∧ 𝜏))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) | ||
| Theorem | 3mix1 1250 | Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
| ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) | ||
| Theorem | 3mix2 1251 | Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
| ⊢ (𝜑 → (𝜓 ∨ 𝜑 ∨ 𝜒)) | ||
| Theorem | 3mix3 1252 | Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
| ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑)) | ||
| Theorem | 3mix1i 1253 | Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.) |
| ⊢ 𝜑 ⇒ ⊢ (𝜑 ∨ 𝜓 ∨ 𝜒) | ||
| Theorem | 3mix2i 1254 | Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.) |
| ⊢ 𝜑 ⇒ ⊢ (𝜓 ∨ 𝜑 ∨ 𝜒) | ||
| Theorem | 3mix3i 1255 | Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.) |
| ⊢ 𝜑 ⇒ ⊢ (𝜓 ∨ 𝜒 ∨ 𝜑) | ||
| Theorem | 3mix1d 1256 | Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃)) | ||
| Theorem | 3mix2d 1257 | Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃)) | ||
| Theorem | 3mix3d 1258 | Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓)) | ||
| Theorem | 3pm3.2i 1259 | Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.) |
| ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 ⇒ ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) | ||
| Theorem | pm3.2an3 1260 | Version of pm3.2 462 for a triple conjunction. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by Kyle Wyonch, 24-Apr-2021.) |
| ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 ∧ 𝜓 ∧ 𝜒)))) | ||
| Theorem | 3jca 1261 | Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
| Theorem | 3jcad 1262 | Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏))) | ||
| Theorem | mpbir3an 1263 | Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.) |
| ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ 𝜑 | ||
| Theorem | mpbir3and 1264 | Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.) (Revised by Mario Carneiro, 9-Jan-2015.) |
| ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) ⇒ ⊢ (𝜑 → 𝜓) | ||
| Theorem | syl3anbrc 1265 | Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜏) | ||
| Theorem | 3anim123i 1266 | Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜏 → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂)) | ||
| Theorem | 3anim1i 1267 | Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
| Theorem | 3anim2i 1268 | Add two conjuncts to antecedent and consequent. (Contributed by AV, 21-Nov-2019.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
| Theorem | 3anim3i 1269 | Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓)) | ||
| Theorem | 3anbi123i 1270 | Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.) |
| ⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜏 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) | ||
| Theorem | 3orbi123i 1271 | Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.) |
| ⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜏 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)) | ||
| Theorem | 3anbi1i 1272 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
| ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
| Theorem | 3anbi2i 1273 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
| ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) ↔ (𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
| Theorem | 3anbi3i 1274 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
| ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓)) | ||
| Theorem | 3imp 1275 | Importation inference. (Contributed by NM, 8-Apr-1994.) |
| ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
| Theorem | 3imp31 1276 | The importation inference 3imp 1275 with commutation of the first and third conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.) |
| ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) | ||
| Theorem | 3imp231 1277 | Importation inference. (Contributed by Alan Sare, 17-Oct-2017.) |
| ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) | ||
| Theorem | 3impa 1278 | Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
| Theorem | 3impb 1279 | Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
| Theorem | 3impia 1280 | Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) |
| ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
| Theorem | 3impib 1281 | Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) |
| ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
| Theorem | ex3 1282 | Apply ex 449 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 | 3exp 1283 | Exportation inference. (Contributed by NM, 30-May-1994.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | ||
| Theorem | 3expa 1284 | Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
| Theorem | 3expb 1285 | Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | ||
| Theorem | 3expia 1286 | Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) | ||
| Theorem | 3expib 1287 | Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | ||
| Theorem | 3com12 1288 | Commutation in antecedent. Swap 1st and 2nd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) | ||
| Theorem | 3com13 1289 | Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) | ||
| Theorem | 3comr 1290 | Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.) (Revised by Wolf Lammen, 9-Apr-2022.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) | ||
| Theorem | 3com23 1291 | Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 9-Apr-2022.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) | ||
| Theorem | 3coml 1292 | Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) | ||
| Theorem | 3com23OLD 1293 | Obsolete version of 3com23 1291 as of 9-Apr-2022. (Contributed by NM, 28-Jan-1996.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) | ||
| Theorem | 3comrOLD 1294 | Obsolete version of 3comr 1290 as of 9-Apr-2022. (Contributed by NM, 28-Jan-1996.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) | ||
| Theorem | 3adant3r1 1295 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) | ||
| Theorem | 3adant3r2 1296 | Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) | ||
| Theorem | 3adant3r3 1297 | Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) | ||
| Theorem | 3imp21 1298 | The importation inference 3imp 1275 with commutation of the first and second conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.) |
| ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) | ||
| Theorem | 3imp3i2an 1299 | An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 13-Apr-2022.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) & ⊢ ((𝜑 ∧ 𝜒) → 𝜏) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜂) | ||
| Theorem | 3imp3i2anOLD 1300 | Obsolete version of 3imp3i2an 1299 as of 13-Apr-2022. (Contributed by Alan Sare, 17-Oct-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) & ⊢ ((𝜑 ∧ 𝜒) → 𝜏) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜂) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |