![]() |
Metamath
Proof Explorer Theorem List (p. 442 of 482) | < 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: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | e3bir 44101 | Right biconditional form of e3 44099. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ (𝜏 ↔ 𝜃) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜏 ) | ||
Theorem | e03 44102 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee03 44103 | e03 44102 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) & ⊢ (𝜑 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e03an 44104 | Conjunction form of e03 44102. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee03an 44105 | Conjunction form of ee03 44103. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e30 44106 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee30 44107 | e30 44106 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ 𝜏 & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e30an 44108 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee30an 44109 | Conjunction form of ee30 44107. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ 𝜏 & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e13 44110 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | e13an 44111 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee13an 44112 | e13an 44111 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e31 44113 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee31 44114 | e31 44113 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e31an 44115 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee31an 44116 | e31an 44115 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → 𝜏) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e23 44117 | 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 44118 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee23an 44119 | e23an 44118 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂))) | ||
Theorem | e32 44120 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee32 44121 | e32 44120 without virtual deductions. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e32an 44122 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee32an 44123 | e33an 44097 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e123 44124 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜒 , 𝜏 ▶ 𝜂 ) & ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜏 ▶ 𝜁 ) | ||
Theorem | ee123 44125 | e123 44124 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) & ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜁))) | ||
Theorem | el123 44126 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜏 ▶ 𝜂 ) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ( ( 𝜑 , 𝜒 , 𝜏 ) ▶ 𝜁 ) | ||
Theorem | e233 44127 | A virtual deduction elimination rule. (Contributed by Alan Sare, 29-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜂 ) & ⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜁 ) | ||
Theorem | e323 44128 | A virtual deduction elimination rule. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) & ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜁 ) | ||
Theorem | e000 44129 | A virtual deduction elimination rule. The non-virtual deduction form of e000 44129 is the virtual deduction form. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ 𝜃 | ||
Theorem | e00 44130 | 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 44131 | Elimination rule identical to mp2an 691. The non-virtual deduction form is the virtual deduction form, which is mp2an 691. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | eel00cT 44132 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (⊤ → 𝜒) | ||
Theorem | eelTT 44133 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (⊤ → 𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | e0a 44134 | 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 44135 | An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | eel0cT 44136 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (⊤ → 𝜓) | ||
Theorem | eelT0 44137 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | e0bi 44138 | Elimination rule identical to mpbi 229. The non-virtual deduction form is the virtual deduction form, which is mpbi 229. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | e0bir 44139 | Elimination rule identical to mpbir 230. The non-virtual deduction form is the virtual deduction form, which is mpbir 230. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 ↔ 𝜑) ⇒ ⊢ 𝜓 | ||
Theorem | uun0.1 44140 | Convention notation form of un0.1 44141. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜓 → 𝜒) & ⊢ ((⊤ ∧ 𝜓) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
Theorem | un0.1 44141 | ⊤ is the constant true, a tautology (see df-tru 1537). 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 44142 | 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 1537. (Revised by David A. Wheeler, 8-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((⊤ ∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | uunT1p1 44143 | 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 44144 | 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 44145 | 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 44146 | 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 44147 | 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 44148 | 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 44149 | A deduction unionizing a non-unionized collection of virtual hypotheses. This would have been named uun221 if the zeroth permutation did not exist in set.mm as anabss7 672. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜓 ∧ 𝜑) ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) | ||
Theorem | un10 44150 | A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( 𝜑 , ⊤ ) ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ 𝜓 ) | ||
Theorem | un01 44151 | A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( ⊤ , 𝜑 ) ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ 𝜓 ) | ||
Theorem | un2122 44152 | 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 44153 | 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 44154 | 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 44155 | 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 44156 | 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 44157 | 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 44158 | 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 44159 | 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 44160 | 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 44161 | 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 44162 | 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 44163 | 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 44164 | 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 44165 | 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 44166 | 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 44167 | 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 44168 | A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1417 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 44169 | 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 44170 | 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 44171 | 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 44172 | 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 44173 | 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 44174 | 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 44175 | 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 44176 | 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 44177 | 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 44178 | A deduction unionizing a non-unionized collection of virtual hypotheses. Commuted version of 3impdir 1349. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜒 ∧ 𝜓) ∧ (𝜑 ∧ 𝜓)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) | ||
Theorem | 3impcombi 44179 | A 1-hypothesis propositional calculus deduction. (Contributed by Alan Sare, 25-Sep-2017.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | trsspwALT 44180 | Virtual deduction proof of the left-to-right implication of dftr4 5266. A transitive class is a subset of its power class. This proof corresponds to the virtual deduction proof of dftr4 5266 without accumulating results. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) | ||
Theorem | trsspwALT2 44181 | Virtual deduction proof of trsspwALT 44180. This proof is the same as the proof of trsspwALT 44180 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 44182 | Short predicate calculus proof of the left-to-right implication of dftr4 5266. 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 44181, which is the virtual deduction proof trsspwALT 44180 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) | ||
Theorem | sspwtr 44183 | Virtual deduction proof of the right-to-left implication of dftr4 5266. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 44183 without accumulating results. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) | ||
Theorem | sspwtrALT 44184 | Virtual deduction proof of sspwtr 44183. This proof is the same as the proof of sspwtr 44183 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 44185 | Short predicate calculus proof of the right-to-left implication of dftr4 5266. 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 44184, which is the virtual deduction proof sspwtr 44183 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) | ||
Theorem | pwtrVD 44186 | Virtual deduction proof of pwtr 5448; see pwtrrVD 44187 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Tr 𝐴 → Tr 𝒫 𝐴) | ||
Theorem | pwtrrVD 44187 | Virtual deduction proof of pwtr 5448; see pwtrVD 44186 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Tr 𝒫 𝐴 → Tr 𝐴) | ||
Theorem | suctrALT 44188 | 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 44188 using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/suctrro.html 44188 is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. See suctr 6449 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 44189 | Virtual deduction proof of snssiALT 44190. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) | ||
Theorem | snssiALT 44190 | If a class is an element of another class, then its singleton is a subclass of that other class. Alternate proof of snssi 4807. This theorem was automatically generated from snssiALTVD 44189 using a translation program. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) | ||
Theorem | snsslVD 44191 | Virtual deduction proof of snssl 44192. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ({𝐴} ⊆ 𝐵 → 𝐴 ∈ 𝐵) | ||
Theorem | snssl 44192 | 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 4785. The proof of this theorem was automatically generated from snsslVD 44191 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 44193 | Virtual deduction proof of snelpwi 5439. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) | ||
Theorem | unipwrVD 44194 | Virtual deduction proof of unipwr 44195. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ⊆ ∪ 𝒫 𝐴 | ||
Theorem | unipwr 44195 | A class is a subclass of the union of its power class. This theorem is the right-to-left subclass lemma of unipw 5446. The proof of this theorem was automatically generated from unipwrVD 44194 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 44196 | Virtual deduction proof of sstrALT2 44197. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | ||
Theorem | sstrALT2 44197 | Virtual deduction proof of sstr 3986, transitivity of subclasses, Theorem 6 of [Suppes] p. 23. This theorem was automatically generated from sstrALT2VD 44196 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 44198 | Virtual deduction proof of suctrALT2 44199. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Tr 𝐴 → Tr suc 𝐴) | ||
Theorem | suctrALT2 44199 | Virtual deduction proof of suctr 6449. The sucessor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD 44198 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 44200* | Virtual deduction proof of elex2 2807. (Contributed by Alan Sare, 25-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |