Home | Metamath
Proof Explorer Theorem List (p. 14 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 | ad5ant13 1301 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
Theorem | ad5ant14 1302 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒) | ||
Theorem | ad5ant15 1303 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒) | ||
Theorem | ad5ant23 1304 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
Theorem | ad5ant24 1305 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒) | ||
Theorem | ad5ant25 1306 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒) | ||
Theorem | ad5ant245 1307 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((((𝜏 ∧ 𝜑) ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | ad5ant234 1308 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) ∧ 𝜂) → 𝜃) | ||
Theorem | ad5ant235 1309 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜂) ∧ 𝜒) → 𝜃) | ||
Theorem | ad5ant123 1310 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜃) | ||
Theorem | ad5ant124 1311 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) ∧ 𝜂) → 𝜃) | ||
Theorem | ad5ant125 1312 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜂) ∧ 𝜒) → 𝜃) | ||
Theorem | ad5ant134 1313 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) ∧ 𝜂) → 𝜃) | ||
Theorem | ad5ant135 1314 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) ∧ 𝜒) → 𝜃) | ||
Theorem | ad5ant145 1315 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((((𝜑 ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | ad5ant1345 1316 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | ad5ant2345 1317 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((((𝜂 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | 3adant1l 1318 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant1r 1319 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant2l 1320 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant2r 1321 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant3l 1322 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adant3r 1323 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) | ||
Theorem | syl12anc 1324 | Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | syl21anc 1325 | Syllogism combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | syl3anc 1326 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | syl22anc 1327 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | syl13anc 1328 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | syl31anc 1329 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | syl112anc 1330 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | syl121anc 1331 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | syl211anc 1332 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | syl23anc 1333 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
Theorem | syl32anc 1334 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
Theorem | syl122anc 1335 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
Theorem | syl212anc 1336 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
Theorem | syl221anc 1337 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
Theorem | syl113anc 1338 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
Theorem | syl131anc 1339 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
Theorem | syl311anc 1340 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
Theorem | syl33anc 1341 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
Theorem | syl222anc 1342 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
Theorem | syl123anc 1343 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
Theorem | syl132anc 1344 | Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
Theorem | syl213anc 1345 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
Theorem | syl231anc 1346 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
Theorem | syl312anc 1347 | Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
Theorem | syl321anc 1348 | Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
Theorem | syl133anc 1349 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) | ||
Theorem | syl313anc 1350 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) | ||
Theorem | syl331anc 1351 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) | ||
Theorem | syl223anc 1352 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) | ||
Theorem | syl232anc 1353 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) | ||
Theorem | syl322anc 1354 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) | ||
Theorem | syl233anc 1355 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (𝜑 → 𝜌) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) | ||
Theorem | syl323anc 1356 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (𝜑 → 𝜌) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) | ||
Theorem | syl332anc 1357 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (𝜑 → 𝜌) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) | ||
Theorem | syl333anc 1358 | A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (𝜑 → 𝜌) & ⊢ (𝜑 → 𝜇) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌 ∧ 𝜇)) → 𝜆) ⇒ ⊢ (𝜑 → 𝜆) | ||
Theorem | syl3an1 1359 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an2 1360 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
⊢ (𝜑 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an3 1361 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
⊢ (𝜑 → 𝜃) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) | ||
Theorem | syl3an1b 1362 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an2b 1363 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
⊢ (𝜑 ↔ 𝜒) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an3b 1364 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
⊢ (𝜑 ↔ 𝜃) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) | ||
Theorem | syl3an1br 1365 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an2br 1366 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
⊢ (𝜒 ↔ 𝜑) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an3br 1367 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
⊢ (𝜃 ↔ 𝜑) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) | ||
Theorem | syl3an 1368 | A triple syllogism inference. (Contributed by NM, 13-May-2004.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜏 → 𝜂) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | syl3anb 1369 | A triple syllogism inference. (Contributed by NM, 15-Oct-2005.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜏 ↔ 𝜂) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | syl3anbr 1370 | A triple syllogism inference. (Contributed by NM, 29-Dec-2011.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜒) & ⊢ (𝜂 ↔ 𝜏) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | syld3an3 1371 | A syllogism inference. (Contributed by NM, 20-May-2007.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) | ||
Theorem | syld3an1 1372 | A syllogism inference. (Contributed by NM, 7-Jul-2008.) |
⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏) | ||
Theorem | syld3an2 1373 | A syllogism inference. (Contributed by NM, 20-May-2007.) |
⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3anl1 1374 | A syllogism inference. (Contributed by NM, 24-Feb-2005.) |
⊢ (𝜑 → 𝜓) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) | ||
Theorem | syl3anl2 1375 | A syllogism inference. (Contributed by NM, 24-Feb-2005.) |
⊢ (𝜑 → 𝜒) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜃) ∧ 𝜏) → 𝜂) | ||
Theorem | syl3anl3 1376 | A syllogism inference. (Contributed by NM, 24-Feb-2005.) |
⊢ (𝜑 → 𝜃) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜑) ∧ 𝜏) → 𝜂) | ||
Theorem | syl3anl 1377 | A triple syllogism inference. (Contributed by NM, 24-Dec-2006.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜏 → 𝜂) & ⊢ (((𝜓 ∧ 𝜃 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ 𝜁) → 𝜎) | ||
Theorem | syl3anr1 1378 | A syllogism inference. (Contributed by NM, 31-Jul-2007.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃 ∧ 𝜏)) → 𝜂) | ||
Theorem | syl3anr2 1379 | A syllogism inference. (Contributed by NM, 1-Aug-2007.) |
⊢ (𝜑 → 𝜃) & ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑 ∧ 𝜏)) → 𝜂) | ||
Theorem | syl3anr3 1380 | A syllogism inference. (Contributed by NM, 23-Aug-2007.) |
⊢ (𝜑 → 𝜏) & ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜑)) → 𝜂) | ||
Theorem | 3impdi 1381 | Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3impdir 1382 | Importation inference (undistribute conjunction). (Contributed by NM, 20-Aug-1995.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) | ||
Theorem | 3anidm12 1383 | Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.) |
⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | 3anidm13 1384 | Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | 3anidm23 1385 | Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | syl2an3an 1386 | syl3an 1368 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜃 → 𝜏) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜃) → 𝜂) | ||
Theorem | syl2an23an 1387 | Deduction related to syl3an 1368 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜃 ∧ 𝜑) → 𝜏) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜃 ∧ 𝜑) → 𝜂) | ||
Theorem | 3ori 1388 | Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006.) |
⊢ (𝜑 ∨ 𝜓 ∨ 𝜒) ⇒ ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒) | ||
Theorem | 3jao 1389 | Disjunction of three antecedents. (Contributed by NM, 8-Apr-1994.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)) | ||
Theorem | 3jaob 1390 | Disjunction of three antecedents. (Contributed by NM, 13-Sep-2011.) |
⊢ (((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))) | ||
Theorem | 3jaoi 1391 | Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜓) & ⊢ (𝜃 → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) | ||
Theorem | 3jaod 1392 | Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜒)) & ⊢ (𝜑 → (𝜏 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) | ||
Theorem | 3jaoian 1393 | Disjunction of three antecedents (inference). (Contributed by NM, 14-Oct-2005.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜃 ∧ 𝜓) → 𝜒) & ⊢ ((𝜏 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜑 ∨ 𝜃 ∨ 𝜏) ∧ 𝜓) → 𝜒) | ||
Theorem | 3jaodan 1394 | Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜒) & ⊢ ((𝜑 ∧ 𝜏) → 𝜒) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒) | ||
Theorem | mpjao3dan 1395 | Eliminate a three-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜒) & ⊢ ((𝜑 ∧ 𝜏) → 𝜒) & ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | 3jaao 1396 | Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜒)) & ⊢ (𝜂 → (𝜁 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜂) → ((𝜓 ∨ 𝜏 ∨ 𝜁) → 𝜒)) | ||
Theorem | syl3an9b 1397 | Nested syllogism inference conjoining 3 dissimilar antecedents. (Contributed by NM, 1-May-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜒 ↔ 𝜏)) & ⊢ (𝜂 → (𝜏 ↔ 𝜁)) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜂) → (𝜓 ↔ 𝜁)) | ||
Theorem | 3orbi123d 1398 | Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) & ⊢ (𝜑 → (𝜂 ↔ 𝜁)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁))) | ||
Theorem | 3anbi123d 1399 | Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) & ⊢ (𝜑 → (𝜂 ↔ 𝜁)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁))) | ||
Theorem | 3anbi12d 1400 | Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |