![]() |
Metamath
Proof Explorer Theorem List (p. 436 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | e03 43501 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜑 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee03 43502 | e03 43501 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) & ⊢ (𝜑 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e03an 43503 | Conjunction form of e03 43501. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜓 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee03an 43504 | Conjunction form of ee03 43502. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏))) & ⊢ ((𝜑 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e30 43505 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee30 43506 | e30 43505 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ 𝜏 & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e30an 43507 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ 𝜏 & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee30an 43508 | Conjunction form of ee30 43506. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ 𝜏 & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e13 43509 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜓 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | e13an 43510 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee13an 43511 | e13an 43510 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂))) | ||
Theorem | e31 43512 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee31 43513 | e31 43512 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → 𝜏) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e31an 43514 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee31an 43515 | e31an 43514 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → 𝜏) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e23 43516 | 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 43517 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜂 ) | ||
Theorem | ee23an 43518 | e23an 43517 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂))) | ||
Theorem | e32 43519 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee32 43520 | e32 43519 without virtual deductions. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e32an 43521 | A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) | ||
Theorem | ee32an 43522 | e33an 43496 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) | ||
Theorem | e123 43523 | A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜒 , 𝜏 ▶ 𝜂 ) & ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜏 ▶ 𝜁 ) | ||
Theorem | ee123 43524 | e123 43523 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) & ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜁))) | ||
Theorem | el123 43525 | A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜏 ▶ 𝜂 ) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ( ( 𝜑 , 𝜒 , 𝜏 ) ▶ 𝜁 ) | ||
Theorem | e233 43526 | A virtual deduction elimination rule. (Contributed by Alan Sare, 29-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜂 ) & ⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜁 ) | ||
Theorem | e323 43527 | A virtual deduction elimination rule. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) & ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜁 ) | ||
Theorem | e000 43528 | A virtual deduction elimination rule. The non-virtual deduction form of e000 43528 is the virtual deduction form. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ 𝜃 | ||
Theorem | e00 43529 | 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 43530 | 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 43531 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (⊤ → 𝜒) | ||
Theorem | eelTT 43532 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (⊤ → 𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | e0a 43533 | 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 43534 | An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | eel0cT 43535 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (⊤ → 𝜓) | ||
Theorem | eelT0 43536 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | e0bi 43537 | 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 43538 | 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 43539 | Convention notation form of un0.1 43540. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (⊤ → 𝜑) & ⊢ (𝜓 → 𝜒) & ⊢ ((⊤ ∧ 𝜓) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
Theorem | un0.1 43540 | ⊤ is the constant true, a tautology (see df-tru 1545). 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 43541 | 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 1545. (Revised by David A. Wheeler, 8-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((⊤ ∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | uunT1p1 43542 | 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 43543 | 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 43544 | 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 43545 | 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 43546 | 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 43547 | 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 43548 | 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 43549 | A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( 𝜑 , ⊤ ) ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ 𝜓 ) | ||
Theorem | un01 43550 | A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ( ⊤ , 𝜑 ) ▶ 𝜓 ) ⇒ ⊢ ( 𝜑 ▶ 𝜓 ) | ||
Theorem | un2122 43551 | 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 43552 | 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 43553 | 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 43554 | 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 43555 | 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 43556 | 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 43557 | 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 43558 | 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 43559 | 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 43560 | 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 43561 | 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 43562 | 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 43563 | 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 43564 | 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 43565 | 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 43566 | 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 43567 | A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1420 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 43568 | 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 43569 | 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 43570 | 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 43571 | 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 43572 | 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 43573 | 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 43574 | 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 43575 | 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 43576 | 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 43577 | A deduction unionizing a non-unionized collection of virtual hypotheses. Commuted version of 3impdir 1352. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜒 ∧ 𝜓) ∧ (𝜑 ∧ 𝜓)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) | ||
Theorem | 3impcombi 43578 | A 1-hypothesis propositional calculus deduction. (Contributed by Alan Sare, 25-Sep-2017.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | trsspwALT 43579 | Virtual deduction proof of the left-to-right implication of dftr4 5273. A transitive class is a subset of its power class. This proof corresponds to the virtual deduction proof of dftr4 5273 without accumulating results. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) | ||
Theorem | trsspwALT2 43580 | Virtual deduction proof of trsspwALT 43579. This proof is the same as the proof of trsspwALT 43579 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 43581 | Short predicate calculus proof of the left-to-right implication of dftr4 5273. 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 43580, which is the virtual deduction proof trsspwALT 43579 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) | ||
Theorem | sspwtr 43582 | Virtual deduction proof of the right-to-left implication of dftr4 5273. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 43582 without accumulating results. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) | ||
Theorem | sspwtrALT 43583 | Virtual deduction proof of sspwtr 43582. This proof is the same as the proof of sspwtr 43582 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 43584 | Short predicate calculus proof of the right-to-left implication of dftr4 5273. 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 43583, which is the virtual deduction proof sspwtr 43582 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) | ||
Theorem | pwtrVD 43585 | Virtual deduction proof of pwtr 5453; see pwtrrVD 43586 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Tr 𝐴 → Tr 𝒫 𝐴) | ||
Theorem | pwtrrVD 43586 | Virtual deduction proof of pwtr 5453; see pwtrVD 43585 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (Tr 𝒫 𝐴 → Tr 𝐴) | ||
Theorem | suctrALT 43587 | 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 43587 using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/suctrro.html 43587 is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. See suctr 6451 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 43588 | Virtual deduction proof of snssiALT 43589. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) | ||
Theorem | snssiALT 43589 | If a class is an element of another class, then its singleton is a subclass of that other class. Alternate proof of snssi 4812. This theorem was automatically generated from snssiALTVD 43588 using a translation program. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) | ||
Theorem | snsslVD 43590 | Virtual deduction proof of snssl 43591. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ({𝐴} ⊆ 𝐵 → 𝐴 ∈ 𝐵) | ||
Theorem | snssl 43591 | 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 4790. The proof of this theorem was automatically generated from snsslVD 43590 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 43592 | Virtual deduction proof of snelpwi 5444. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) | ||
Theorem | unipwrVD 43593 | Virtual deduction proof of unipwr 43594. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ⊆ ∪ 𝒫 𝐴 | ||
Theorem | unipwr 43594 | A class is a subclass of the union of its power class. This theorem is the right-to-left subclass lemma of unipw 5451. The proof of this theorem was automatically generated from unipwrVD 43593 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 43595 | Virtual deduction proof of sstrALT2 43596. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | ||
Theorem | sstrALT2 43596 | Virtual deduction proof of sstr 3991, transitivity of subclasses, Theorem 6 of [Suppes] p. 23. This theorem was automatically generated from sstrALT2VD 43595 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 43597 | Virtual deduction proof of suctrALT2 43598. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Tr 𝐴 → Tr suc 𝐴) | ||
Theorem | suctrALT2 43598 | Virtual deduction proof of suctr 6451. The sucessor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD 43597 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 43599* | Virtual deduction proof of elex2 2813. (Contributed by Alan Sare, 25-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) | ||
Theorem | elex22VD 43600* | Virtual deduction proof of elex22 3497. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |