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