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