Home | Metamath
Proof Explorer Theorem List (p. 410 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ee001 40901 | e001 40900 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | e11 40902 | A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ (𝜓 → (𝜒 → 𝜃)) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | e11an 40903 | Conjunction form of e11 40902. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 ▶ 𝜒 ) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | ee11an 40904 | e11an 40903 without virtual deductions. syl22anc 834 is also e11an 40903 without virtual deductions, exept with a different order of hypotheses. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | e01 40905 | A virtual deduction elimination rule. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ (𝜑 → (𝜒 → 𝜃)) ⇒ ⊢ ( 𝜓 ▶ 𝜃 ) | ||
Theorem | e01an 40906 | Conjunction form of e01 40905. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( 𝜓 ▶ 𝜃 ) | ||
Theorem | ee01an 40907 | e01an 40906 without virtual deductions. sylancr 587 is also a form of e01an 40906 without virtual deduction, except the order of the hypotheses is different. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
Theorem | e10 40908 | A virtual deduction elimination rule (see mpisyl 21). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ (𝜓 → (𝜒 → 𝜃)) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | e10an 40909 | Conjunction form of e10 40908. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ 𝜒 & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( 𝜑 ▶ 𝜃 ) | ||
Theorem | ee10an 40910 | e10an 40909 without virtual deductions. sylancl 586 is also e10an 40909 without virtual deductions, except the order of the hypotheses is different. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | e02 40911 | A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜑 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e02an 40912 | Conjunction form of e02 40911. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | ee02an 40913 | e02an 40912 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜓 → (𝜒 → 𝜏)) | ||
Theorem | eel021old 40914 | el021old 40915 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒) → 𝜏) | ||
Theorem | el021old 40915 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( ( 𝜓 , 𝜒 ) ▶ 𝜃 ) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( ( 𝜓 , 𝜒 ) ▶ 𝜏 ) | ||
Theorem | eel132 40916 | syl2an 595 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂) | ||
Theorem | eel000cT 40917 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (⊤ → 𝜃) | ||
Theorem | eel0TT 40918 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (⊤ → 𝜓) & ⊢ (⊤ → 𝜒) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | eelT00 40919 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | eelTTT 40920 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (⊤ → 𝜓) & ⊢ (⊤ → 𝜒) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | eelT11 40921 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → 𝜃) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜓 → 𝜏) | ||
Theorem | eelT1 40922 | Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Alan Sare, 23-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜓 → 𝜒) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
Theorem | eelT12 40923 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜓 → 𝜒) & ⊢ (𝜃 → 𝜏) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜓 ∧ 𝜃) → 𝜂) | ||
Theorem | eelTT1 40924 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (⊤ → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | eelT01 40925 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | eel0T1 40926 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (⊤ → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | eel12131 40927 | An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | eel2131 40928 | syl2an 595 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜂) | ||
Theorem | eel3132 40929 | syl2an 595 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜃 ∧ 𝜓) → 𝜏) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜂) | ||
Theorem | eel0321old 40930 | el0321old 40931 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜂) | ||
Theorem | el0321old 40931 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( ( 𝜓 , 𝜒 , 𝜃 ) ▶ 𝜏 ) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( ( 𝜓 , 𝜒 , 𝜃 ) ▶ 𝜂 ) | ||
Theorem | eel2122old 40932 | el2122old 40933 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ (𝜓 → 𝜃) & ⊢ (𝜓 → 𝜏) & ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜂) | ||
Theorem | el2122old 40933 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜒 ) & ⊢ ( 𝜓 ▶ 𝜃 ) & ⊢ ( 𝜓 ▶ 𝜏 ) & ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( ( 𝜑 , 𝜓 ) ▶ 𝜂 ) | ||
Theorem | eel0000 40934 | Elimination rule similar to mp4an 689, except with a left-nested conjunction unification theorem. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ 𝜏 | ||
Theorem | eel00001 40935 | An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ (𝜏 → 𝜂) & ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜏 → 𝜁) | ||
Theorem | eel00000 40936 | Elimination rule similar eel0000 40934, except with five hpothesis steps. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ 𝜏 & ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ 𝜂 | ||
Theorem | eel11111 40937 | Five-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc 1374 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜑 → 𝜂) & ⊢ (((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) | ||
Theorem | e12 40938 | A virtual deduction elimination rule (see sylsyld 61). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜓 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e12an 40939 | Conjunction form of e12 40938 (see syl6an 680). (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ((𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜒 ▶ 𝜏 ) | ||
Theorem | el12 40940 | Virtual deduction form of syl2an 595. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜏 ▶ 𝜒 ) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ( ( 𝜑 , 𝜏 ) ▶ 𝜃 ) | ||
Theorem | e20 40941 | A virtual deduction elimination rule (see syl6mpi 67). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ (𝜒 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | e20an 40942 | Conjunction form of e20 40941. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ 𝜃 & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | ee20an 40943 | e20an 40942 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ 𝜃 & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → 𝜏)) | ||
Theorem | e21 40944 | A virtual deduction elimination rule (see syl6ci 71). (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ (𝜒 → (𝜃 → 𝜏)) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | e21an 40945 | Conjunction form of e21 40944. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 ▶ 𝜃 ) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) | ||
Theorem | ee21an 40946 | e21an 40945 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) & ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → 𝜏)) | ||
Theorem | e333 40947 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) & ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜁 ) | ||
Theorem | e33 40948 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | e33an 40949 | Conjunction form of e33 40948. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee33an 40950 | e33an 40949 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏))) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e3 40951 | Meta-connective form of syl8 76. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e3bi 40952 | Biconditional form of e3 40951. syl8ib 257 is e3bi 40952 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜃 ↔ 𝜏) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e3bir 40953 | Right biconditional form of e3 40951. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜏 ↔ 𝜃) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e03 40954 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee03 40955 | e03 40954 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) & ⊢ (𝜑 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e03an 40956 | Conjunction form of e03 40954. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee03an 40957 | Conjunction form of ee03 40955. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e30 40958 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee30 40959 | e30 40958 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ 𝜏 & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e30an 40960 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee30an 40961 | Conjunction form of ee30 40959. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ 𝜏 & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e13 40962 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | e13an 40963 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee13an 40964 | e13an 40963 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e31 40965 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee31 40966 | e31 40965 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e31an 40967 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee31an 40968 | e31an 40967 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → 𝜏) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e23 40969 | A virtual deduction elimination rule (see syl10 79). (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜂 ) | ||
Theorem | e23an 40970 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee23an 40971 | e23an 40970 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂))) | ||
Theorem | e32 40972 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee32 40973 | e32 40972 without virtual deductions. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e32an 40974 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee32an 40975 | e33an 40949 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e123 40976 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜒 , 𝜏 ▶ 𝜂 ) & ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜏 ▶ 𝜁 ) | ||
Theorem | ee123 40977 | e123 40976 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) & ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜁))) | ||
Theorem | el123 40978 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜏 ▶ 𝜂 ) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ( ( 𝜑 , 𝜒 , 𝜏 ) ▶ 𝜁 ) | ||
Theorem | e233 40979 | A virtual deduction elimination rule. (Contributed by Alan Sare, 29-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜂 ) & ⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜁 ) | ||
Theorem | e323 40980 | A virtual deduction elimination rule. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) & ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜁 ) | ||
Theorem | e000 40981 | A virtual deduction elimination rule. The non-virtual deduction form of e000 40981 is the virtual deduction form. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ 𝜃 | ||
Theorem | e00 40982 | Elimination rule identical to mp2 9. The non-virtual deduction form is the virtual deduction form, which is mp2 9. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ 𝜒 | ||
Theorem | e00an 40983 | Elimination rule identical to mp2an 688. The non-virtual deduction form is the virtual deduction form, which is mp2an 688. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | eel00cT 40984 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (⊤ → 𝜒) | ||
Theorem | eelTT 40985 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (⊤ → 𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | e0a 40986 | Elimination rule identical to ax-mp 5. The non-virtual deduction form is the virtual deduction form, which is ax-mp 5. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | eelT 40987 | An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | eel0cT 40988 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (⊤ → 𝜓) | ||
Theorem | eelT0 40989 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | e0bi 40990 | Elimination rule identical to mpbi 231. The non-virtual deduction form is the virtual deduction form, which is mpbi 231. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | e0bir 40991 | Elimination rule identical to mpbir 232. The non-virtual deduction form is the virtual deduction form, which is mpbir 232. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 ↔ 𝜑) ⇒ ⊢ 𝜓 | ||
Theorem | uun0.1 40992 | Convention notation form of un0.1 40993. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜓 → 𝜒) & ⊢ ((⊤ ∧ 𝜓) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
Theorem | un0.1 40993 | ⊤ is the constant true, a tautology (see df-tru 1531). Kleene's "empty conjunction" is logically equivalent to ⊤. In a virtual deduction we shall interpret ⊤ to be the empty wff or the empty collection of virtual hypotheses. ⊤ in a virtual deduction translated into conventional notation we shall interpret to be Kleene's empty conjunction. If 𝜃 is true given the empty collection of virtual hypotheses and another collection of virtual hypotheses, then it is true given only the other collection of virtual hypotheses. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ⊤ ▶ 𝜑 ) & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ( ( ⊤ , 𝜓 ) ▶ 𝜃 ) ⇒ ⊢ ( 𝜓 ▶ 𝜃 ) | ||
Theorem | uunT1 40994 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) Proof was revised to accommodate a possible future version of df-tru 1531. (Revised by David A. Wheeler, 8-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((⊤ ∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | uunT1p1 40995 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ ⊤) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | uunT21 40996 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((⊤ ∧ (𝜑 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | uun121 40997 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | uun121p1 40998 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | uun132 40999 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | uun132p1 41000 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |