Home | Metamath
Proof Explorer Theorem List (p. 412 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description | ||||||
---|---|---|---|---|---|---|---|---|
Statement | ||||||||
Theorem | ee30an 41101 | Conjunction form of ee30 41099. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ 𝜏 & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||||||||
Theorem | e13 41102 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||||||||
Theorem | e13an 41103 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||||||||
Theorem | ee13an 41104 | e13an 41103 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂))) | ||||||||
Theorem | e31 41105 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||||||||
Theorem | ee31 41106 | e31 41105 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||||||||
Theorem | e31an 41107 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||||||||
Theorem | ee31an 41108 | e31an 41107 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → 𝜏) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||||||||
Theorem | e23 41109 | 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 41110 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜂 ) | ||||||||
Theorem | ee23an 41111 | e23an 41110 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂))) | ||||||||
Theorem | e32 41112 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||||||||
Theorem | ee32 41113 | e32 41112 without virtual deductions. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||||||||
Theorem | e32an 41114 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||||||||
Theorem | ee32an 41115 | e33an 41089 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||||||||
Theorem | e123 41116 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜒 , 𝜏 ▶ 𝜂 ) & ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜏 ▶ 𝜁 ) | ||||||||
Theorem | ee123 41117 | e123 41116 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) & ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜁))) | ||||||||
Theorem | el123 41118 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜏 ▶ 𝜂 ) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ( ( 𝜑 , 𝜒 , 𝜏 ) ▶ 𝜁 ) | ||||||||
Theorem | e233 41119 | A virtual deduction elimination rule. (Contributed by Alan Sare, 29-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜂 ) & ⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜁 ) | ||||||||
Theorem | e323 41120 | A virtual deduction elimination rule. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) & ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜁 ) | ||||||||
Theorem | e000 41121 | A virtual deduction elimination rule. The non-virtual deduction form of e000 41121 is the virtual deduction form. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ 𝜃 | ||||||||
Theorem | e00 41122 | 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 41123 | Elimination rule identical to mp2an 690. The non-virtual deduction form is the virtual deduction form, which is mp2an 690. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||||||||
Theorem | eel00cT 41124 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (⊤ → 𝜒) | ||||||||
Theorem | eelTT 41125 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (⊤ → 𝜑) & ⊢ (⊤ → 𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||||||||
Theorem | e0a 41126 | 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 41127 | An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (⊤ → 𝜑) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ 𝜓 | ||||||||
Theorem | eel0cT 41128 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ 𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (⊤ → 𝜓) | ||||||||
Theorem | eelT0 41129 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (⊤ → 𝜑) & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||||||||
Theorem | e0bi 41130 | Elimination rule identical to mpbi 232. The non-virtual deduction form is the virtual deduction form, which is mpbi 232. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ 𝜑 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ 𝜓 | ||||||||
Theorem | e0bir 41131 | Elimination rule identical to mpbir 233. The non-virtual deduction form is the virtual deduction form, which is mpbir 233. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ 𝜑 & ⊢ (𝜓 ↔ 𝜑) ⇒ ⊢ 𝜓 | ||||||||
Theorem | uun0.1 41132 | Convention notation form of un0.1 41133. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (⊤ → 𝜑) & ⊢ (𝜓 → 𝜒) & ⊢ ((⊤ ∧ 𝜓) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||||||||
Theorem | un0.1 41133 | ⊤ is the constant true, a tautology (see df-tru 1540). 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 41134 | 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 1540. (Revised by David A. Wheeler, 8-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ((⊤ ∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||||||||
Theorem | uunT1p1 41135 | 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 41136 | 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 41137 | 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 41138 | 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 41139 | 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 41140 | 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 | anabss7p1 41141 | A deduction unionizing a non-unionized collection of virtual hypotheses. This would have been named uun221 if the 0th permutation did not exist in set.mm as anabss7 671. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (((𝜓 ∧ 𝜑) ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) | ||||||||
Theorem | un10 41142 | A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ( ( 𝜑 , ⊤ ) ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ 𝜓 ) | ||||||||
Theorem | un01 41143 | A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ( ( ⊤ , 𝜑 ) ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ 𝜓 ) | ||||||||
Theorem | un2122 41144 | 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.) | ||||||
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||||||||
Theorem | uun2131 41145 | 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 | uun2131p1 41146 | 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 | uunTT1 41147 | 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 | uunTT1p1 41148 | 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 | uunTT1p2 41149 | 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 | uunT11 41150 | 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 | uunT11p1 41151 | 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 | uunT11p2 41152 | 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 | uunT12 41153 | 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 | uunT12p1 41154 | 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 | uunT12p2 41155 | 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 | uunT12p3 41156 | 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 | uunT12p4 41157 | 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 | uunT12p5 41158 | 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 | uun111 41159 | 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 | 3anidm12p1 41160 | A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1415 denotes the deduction which would have been named uun112 if it did not pre-exist in set.mm. This second permutation's name is based on this pre-existing name. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||||||||
Theorem | 3anidm12p2 41161 | 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 | uun123 41162 | 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 | uun123p1 41163 | 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 | uun123p2 41164 | 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 | uun123p3 41165 | 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 | uun123p4 41166 | 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 | uun2221 41167 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 30-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ((𝜑 ∧ 𝜑 ∧ (𝜓 ∧ 𝜑)) → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) | ||||||||
Theorem | uun2221p1 41168 | 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 | uun2221p2 41169 | 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 | 3impdirp1 41170 | A deduction unionizing a non-unionized collection of virtual hypotheses. Commuted version of 3impdir 1347. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (((𝜒 ∧ 𝜓) ∧ (𝜑 ∧ 𝜓)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) | ||||||||
Theorem | 3impcombi 41171 | A 1-hypothesis propositional calculus deduction. (Contributed by Alan Sare, 25-Sep-2017.) | ||||||
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) | ||||||||
Theorem | trsspwALT 41172 | Virtual deduction proof of the left-to-right implication of dftr4 5177. A transitive class is a subset of its power class. This proof corresponds to the virtual deduction proof of dftr4 5177 without accumulating results. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) | ||||||||
Theorem | trsspwALT2 41173 | Virtual deduction proof of trsspwALT 41172. This proof is the same as the proof of trsspwALT 41172 except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A transitive class is a subset of its power class. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) | ||||||||
Theorem | trsspwALT3 41174 | Short predicate calculus proof of the left-to-right implication of dftr4 5177. A transitive class is a subset of its power class. This proof was constructed by applying Metamath's minimize command to the proof of trsspwALT2 41173, which is the virtual deduction proof trsspwALT 41172 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) | ||||||||
Theorem | sspwtr 41175 | Virtual deduction proof of the right-to-left implication of dftr4 5177. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 41175 without accumulating results. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) | ||||||||
Theorem | sspwtrALT 41176 | Virtual deduction proof of sspwtr 41175. This proof is the same as the proof of sspwtr 41175 except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A class which is a subclass of its power class is transitive. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) | ||||||||
Theorem | sspwtrALT2 41177 | Short predicate calculus proof of the right-to-left implication of dftr4 5177. A class which is a subclass of its power class is transitive. This proof was constructed by applying Metamath's minimize command to the proof of sspwtrALT 41176, which is the virtual deduction proof sspwtr 41175 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) | ||||||||
Theorem | pwtrVD 41178 | Virtual deduction proof of pwtr 5345; see pwtrrVD 41179 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (Tr 𝐴 → Tr 𝒫 𝐴) | ||||||||
Theorem | pwtrrVD 41179 | Virtual deduction proof of pwtr 5345; see pwtrVD 41178 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ 𝐴 ∈ V ⇒ ⊢ (Tr 𝒫 𝐴 → Tr 𝐴) | ||||||||
Theorem | suctrALT 41180 | The successor of a transitive class is transitive. The proof of https://us.metamath.org/other/completeusersproof/suctrvd.html is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctrALT 41180 using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/suctrro.html 41180 is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. See suctr 6274 for the original proof. (Contributed by Alan Sare, 11-Apr-2009.) (Revised by Alan Sare, 12-Jun-2018.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (Tr 𝐴 → Tr suc 𝐴) | ||||||||
Theorem | snssiALTVD 41181 | Virtual deduction proof of snssiALT 41182. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) | ||||||||
Theorem | snssiALT 41182 | If a class is an element of another class, then its singleton is a subclass of that other class. Alternate proof of snssi 4741. This theorem was automatically generated from snssiALTVD 41181 using a translation program. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) | ||||||||
Theorem | snsslVD 41183 | Virtual deduction proof of snssl 41184. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ 𝐴 ∈ V ⇒ ⊢ ({𝐴} ⊆ 𝐵 → 𝐴 ∈ 𝐵) | ||||||||
Theorem | snssl 41184 | If a singleton is a subclass of another class, then the singleton's element is an element of that other class. This theorem is the right-to-left implication of the biconditional snss 4718. The proof of this theorem was automatically generated from snsslVD 41183 using a tools command file, translateMWO.cmd, by translating the proof into its non-virtual deduction form and minimizing it. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ 𝐴 ∈ V ⇒ ⊢ ({𝐴} ⊆ 𝐵 → 𝐴 ∈ 𝐵) | ||||||||
Theorem | snelpwrVD 41185 | Virtual deduction proof of snelpwi 5337. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) | ||||||||
Theorem | unipwrVD 41186 | Virtual deduction proof of unipwr 41187. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ 𝐴 ⊆ ∪ 𝒫 𝐴 | ||||||||
Theorem | unipwr 41187 | A class is a subclass of the union of its power class. This theorem is the right-to-left subclass lemma of unipw 5343. The proof of this theorem was automatically generated from unipwrVD 41186 using a tools command file , translateMWO.cmd , by translating the proof into its non-virtual deduction form and minimizing it. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ 𝐴 ⊆ ∪ 𝒫 𝐴 | ||||||||
Theorem | sstrALT2VD 41188 | Virtual deduction proof of sstrALT2 41189. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | ||||||||
Theorem | sstrALT2 41189 | Virtual deduction proof of sstr 3975, transitivity of subclasses, Theorem 6 of [Suppes] p. 23. This theorem was automatically generated from sstrALT2VD 41188 using the command file translate_without_overwriting.cmd . It was not minimized because the automated minimization excluding duplicates generates a minimized proof which, although not directly containing any duplicates, indirectly contains a duplicate. That is, the trace back of the minimized proof contains a duplicate. This is undesirable because some step(s) of the minimized proof use the proven theorem. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | ||||||||
Theorem | suctrALT2VD 41190 | Virtual deduction proof of suctrALT2 41191. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (Tr 𝐴 → Tr suc 𝐴) | ||||||||
Theorem | suctrALT2 41191 | Virtual deduction proof of suctr 6274. The sucessor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD 41190 using the tools command file translate_without_overwriting_minimize_excluding_duplicates.cmd . (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (Tr 𝐴 → Tr suc 𝐴) | ||||||||
Theorem | elex2VD 41192* | Virtual deduction proof of elex2 3516. (Contributed by Alan Sare, 25-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) | ||||||||
Theorem | elex22VD 41193* | Virtual deduction proof of elex22 3517. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | ||||||||
Theorem | eqsbc3rVD 41194* | Virtual deduction proof of eqsbc3r 3837. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴)) | ||||||||
Theorem | zfregs2VD 41195* | Virtual deduction proof of zfregs2 9175. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝐴 ≠ ∅ → ¬ ∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥)) | ||||||||
Theorem | tpid3gVD 41196 | Virtual deduction proof of tpid3g 4708. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) | ||||||||
Theorem | en3lplem1VD 41197* | Virtual deduction proof of en3lplem1 9075. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) | ||||||||
Theorem | en3lplem2VD 41198* | Virtual deduction proof of en3lplem2 9076. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) | ||||||||
Theorem | en3lpVD 41199 | Virtual deduction proof of en3lp 9077. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) | ||||||||
Theorem | simplbi2VD 41200 |
Virtual deduction proof of simplbi2 503. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
| ||||||
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜒 → 𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |