HomeTheorem List (p. 16 of 435)
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. 16 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: | Metamath Proof Explorer
(1-28319) |
Hilbert Space Explorer
(28320-29844) |
Users' Mathboxes
(29845-43440) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | syl32anc 1501 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
| Theorem | syl122anc 1502 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
| Theorem | syl212anc 1503 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
| Theorem | syl221anc 1504 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
| Theorem | syl113anc 1505 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
| Theorem | syl131anc 1506 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
| Theorem | syl311anc 1507 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
| Theorem | syl33anc 1508 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
| Theorem | syl222anc 1509 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
| Theorem | syl123anc 1510 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
| Theorem | syl132anc 1511 | Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
| Theorem | syl213anc 1512 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
| Theorem | syl231anc 1513 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
| Theorem | syl312anc 1514 | Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
| Theorem | syl321anc 1515 | Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) | ||
| Theorem | syl133anc 1516 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) | ||
| Theorem | syl313anc 1517 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) | ||
| Theorem | syl331anc 1518 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) | ||
| Theorem | syl223anc 1519 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) | ||
| Theorem | syl232anc 1520 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) | ||
| Theorem | syl322anc 1521 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) | ||
| Theorem | syl233anc 1522 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (𝜑 → 𝜌) & ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) | ||
| Theorem | syl323anc 1523 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (𝜑 → 𝜌) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) | ||
| Theorem | syl332anc 1524 | Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (𝜑 → 𝜌) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) | ||
| Theorem | syl333anc 1525 | A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (𝜑 → 𝜁) & ⊢ (𝜑 → 𝜎) & ⊢ (𝜑 → 𝜌) & ⊢ (𝜑 → 𝜇) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌 ∧ 𝜇)) → 𝜆) ⇒ ⊢ (𝜑 → 𝜆) | ||
| Theorem | syl3an1b 1526 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
| ⊢ (𝜑 ↔ 𝜓) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | syl3an2b 1527 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
| ⊢ (𝜑 ↔ 𝜒) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) | ||
| Theorem | syl3an3b 1528 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
| ⊢ (𝜑 ↔ 𝜃) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) | ||
| Theorem | syl3an1br 1529 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
| ⊢ (𝜓 ↔ 𝜑) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | syl3an2br 1530 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
| ⊢ (𝜒 ↔ 𝜑) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) | ||
| Theorem | syl3an3br 1531 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
| ⊢ (𝜃 ↔ 𝜑) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) | ||
| Theorem | syld3an3 1532 | A syllogism inference. (Contributed by NM, 20-May-2007.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) | ||
| Theorem | syld3an1 1533 | A syllogism inference. (Contributed by NM, 7-Jul-2008.) (Proof shortened by Wolf Lammen, 26-Jun-2022.) |
| ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏) | ||
| Theorem | syld3an1OLD 1534 | Obsolete version of syld3an1 1533 as of 26-Jun-2022. (Contributed by NM, 7-Jul-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏) | ||
| Theorem | syld3an2 1535 | A syllogism inference. (Contributed by NM, 20-May-2007.) |
| ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | syld3an2OLD 1536 | Obsolete version of syld3an2 1535 as of 26-Jun-2022. (Contributed by NM, 7-Jul-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
| Theorem | syl3anl1 1537 | A syllogism inference. (Contributed by NM, 24-Feb-2005.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) | ||
| Theorem | syl3anl2 1538 | A syllogism inference. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 27-Jun-2022.) |
| ⊢ (𝜑 → 𝜒) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜃) ∧ 𝜏) → 𝜂) | ||
| Theorem | syl3anl2OLD 1539 | Obsolete version of syl3anl2 1538 as of 27-Jun-2022. (Contributed by NM, 24-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝜒) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜃) ∧ 𝜏) → 𝜂) | ||
| Theorem | syl3anl3 1540 | A syllogism inference. (Contributed by NM, 24-Feb-2005.) |
| ⊢ (𝜑 → 𝜃) & ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜑) ∧ 𝜏) → 𝜂) | ||
| Theorem | syl3anl 1541 | A triple syllogism inference. (Contributed by NM, 24-Dec-2006.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜏 → 𝜂) & ⊢ (((𝜓 ∧ 𝜃 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ 𝜁) → 𝜎) | ||
| Theorem | syl3anr1 1542 | A syllogism inference. (Contributed by NM, 31-Jul-2007.) |
| ⊢ (𝜑 → 𝜓) & ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃 ∧ 𝜏)) → 𝜂) | ||
| Theorem | syl3anr2 1543 | A syllogism inference. (Contributed by NM, 1-Aug-2007.) (Proof shortened by Wolf Lammen, 27-Jun-2022.) |
| ⊢ (𝜑 → 𝜃) & ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑 ∧ 𝜏)) → 𝜂) | ||
| Theorem | syl3anr2OLD 1544 | Obsolete version of syl3anr2 1543 as of 27-Jun-2022. (Contributed by NM, 1-Aug-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝜃) & ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑 ∧ 𝜏)) → 𝜂) | ||
| Theorem | syl3anr3 1545 | A syllogism inference. (Contributed by NM, 23-Aug-2007.) |
| ⊢ (𝜑 → 𝜏) & ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜑)) → 𝜂) | ||
| Theorem | 3anidm12 1546 | Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.) |
| ⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
| Theorem | 3anidm13 1547 | Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
| Theorem | 3anidm23 1548 | Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
| Theorem | syl2an3an 1549 | syl3an 1203 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜃 → 𝜏) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜃) → 𝜂) | ||
| Theorem | syl2an23an 1550 | Deduction related to syl3an 1203 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Jun-2022.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜃 ∧ 𝜑) → 𝜏) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜃 ∧ 𝜑) → 𝜂) | ||
| Theorem | syl2an23anOLD 1551 | Obsolete version of syl2an23an 1550 as of 28-Jun-2022. (Contributed by Alan Sare, 31-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜃 ∧ 𝜑) → 𝜏) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜃 ∧ 𝜑) → 𝜂) | ||
| Theorem | 3ori 1552 | Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006.) |
| ⊢ (𝜑 ∨ 𝜓 ∨ 𝜒) ⇒ ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒) | ||
| Theorem | 3jao 1553 | Disjunction of three antecedents. (Contributed by NM, 8-Apr-1994.) |
| ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)) | ||
| Theorem | 3jaoOLD 1554 | Obsolete version of 3jao 1553 as of 28-Jun-2022. (Contributed by NM, 8-Apr-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)) | ||
| Theorem | 3jaob 1555 | Disjunction of three antecedents. (Contributed by NM, 13-Sep-2011.) |
| ⊢ (((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))) | ||
| Theorem | 3jaoi 1556 | Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜓) & ⊢ (𝜃 → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) | ||
| Theorem | 3jaod 1557 | Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜒)) & ⊢ (𝜑 → (𝜏 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) | ||
| Theorem | 3jaoian 1558 | Disjunction of three antecedents (inference). (Contributed by NM, 14-Oct-2005.) |
| ⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜃 ∧ 𝜓) → 𝜒) & ⊢ ((𝜏 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜑 ∨ 𝜃 ∨ 𝜏) ∧ 𝜓) → 𝜒) | ||
| Theorem | 3jaodan 1559 | Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005.) |
| ⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜒) & ⊢ ((𝜑 ∧ 𝜏) → 𝜒) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒) | ||
| Theorem | mpjao3dan 1560 | Eliminate a three-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.) |
| ⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜒) & ⊢ ((𝜑 ∧ 𝜏) → 𝜒) & ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏)) ⇒ ⊢ (𝜑 → 𝜒) | ||
| Theorem | 3jaao 1561 | 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 1562 | Nested syllogism inference conjoining 3 dissimilar antecedents. (Contributed by NM, 1-May-1995.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜒 ↔ 𝜏)) & ⊢ (𝜂 → (𝜏 ↔ 𝜁)) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜂) → (𝜓 ↔ 𝜁)) | ||
| Theorem | 3orbi123d 1563 | Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) & ⊢ (𝜑 → (𝜂 ↔ 𝜁)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁))) | ||
| Theorem | 3anbi123d 1564 | Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) & ⊢ (𝜑 → (𝜂 ↔ 𝜁)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁))) | ||
| Theorem | 3anbi12d 1565 | Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜂))) | ||
| Theorem | 3anbi13d 1566 | Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏))) | ||
| Theorem | 3anbi23d 1567 | Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜂 ∧ 𝜓 ∧ 𝜃) ↔ (𝜂 ∧ 𝜒 ∧ 𝜏))) | ||
| Theorem | 3anbi1d 1568 | Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) | ||
| Theorem | 3anbi2d 1569 | Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏))) | ||
| Theorem | 3anbi3d 1570 | Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.) |
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∧ 𝜏 ∧ 𝜓) ↔ (𝜃 ∧ 𝜏 ∧ 𝜒))) | ||
| Theorem | 3anim123d 1571 | Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜑 → (𝜂 → 𝜁)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) → (𝜒 ∧ 𝜏 ∧ 𝜁))) | ||
| Theorem | 3orim123d 1572 | Deduction joining 3 implications to form implication of disjunctions. (Contributed by NM, 4-Apr-1997.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜑 → (𝜂 → 𝜁)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) → (𝜒 ∨ 𝜏 ∨ 𝜁))) | ||
| Theorem | an6 1573 | Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995.) |
| ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏) ∧ (𝜒 ∧ 𝜂))) | ||
| Theorem | 3an6 1574 | Analogue of an4 646 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ (𝜓 ∧ 𝜃 ∧ 𝜂))) | ||
| Theorem | 3or6 1575 | Analogue of or4 955 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) |
| ⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃) ∨ (𝜏 ∨ 𝜂)) ↔ ((𝜑 ∨ 𝜒 ∨ 𝜏) ∨ (𝜓 ∨ 𝜃 ∨ 𝜂))) | ||
| Theorem | mp3an1 1576 | An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
| ⊢ 𝜑 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | ||
| Theorem | mp3an2 1577 | An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
| ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | ||
| Theorem | mp3an3 1578 | An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
| ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | ||
| Theorem | mp3an12 1579 | An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.) |
| ⊢ 𝜑 & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜒 → 𝜃) | ||
| Theorem | mp3an13 1580 | An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
| ⊢ 𝜑 & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
| Theorem | mp3an23 1581 | An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
| ⊢ 𝜓 & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
| Theorem | mp3an1i 1582 | An inference based on modus ponens. (Contributed by NM, 5-Jul-2005.) |
| ⊢ 𝜓 & ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏)) | ||
| Theorem | mp3anl1 1583 | An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.) |
| ⊢ 𝜑 & ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
| Theorem | mp3anl2 1584 | An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.) |
| ⊢ 𝜓 & ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
| Theorem | mp3anl3 1585 | An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.) |
| ⊢ 𝜒 & ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏) | ||
| Theorem | mp3anr1 1586 | An inference based on modus ponens. (Contributed by NM, 4-Nov-2006.) |
| ⊢ 𝜓 & ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜃)) → 𝜏) | ||
| Theorem | mp3anr2 1587 | An inference based on modus ponens. (Contributed by NM, 24-Nov-2006.) |
| ⊢ 𝜒 & ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜏) | ||
| Theorem | mp3anr3 1588 | An inference based on modus ponens. (Contributed by NM, 19-Oct-2007.) |
| ⊢ 𝜃 & ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏) | ||
| Theorem | mp3an 1589 | An inference based on modus ponens. (Contributed by NM, 14-May-1999.) |
| ⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ 𝜃 | ||
| Theorem | mpd3an3 1590 | An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.) |
| ⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | ||
| Theorem | mpd3an23 1591 | An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
| Theorem | mp3and 1592 | A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016.) |
| ⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜑 → 𝜏) | ||
| Theorem | mp3an12i 1593 | mp3an 1589 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.) |
| ⊢ 𝜑 & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜒 → 𝜏) | ||
| Theorem | mp3an2i 1594 | mp3an 1589 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.) |
| ⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → 𝜃) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜓 → 𝜏) | ||
| Theorem | mp3an3an 1595 | mp3an 1589 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.) |
| ⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ (𝜃 → 𝜏) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜓 ∧ 𝜃) → 𝜂) | ||
| Theorem | mp3an2ani 1596 | An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) |
| ⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ ((𝜓 ∧ 𝜃) → 𝜏) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜓 ∧ 𝜃) → 𝜂) | ||
| Theorem | biimp3a 1597 | Infer implication from a logical equivalence. Similar to biimpa 470. (Contributed by NM, 4-Sep-2005.) |
| ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
| Theorem | biimp3ar 1598 | Infer implication from a logical equivalence. Similar to biimpar 471. (Contributed by NM, 2-Jan-2009.) |
| ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | ||
| Theorem | 3anandis 1599 | Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 18-Apr-2007.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒) ∧ (𝜑 ∧ 𝜃)) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) | ||
| Theorem | 3anandirs 1600 | Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 25-Jul-2006.) |
| ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |