P. 381 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38001-38100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	e31an 38001	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee31an 38002	e31an 38001 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e23 38003	A virtual deduction elimination rule (see syl10 77). (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜂   )
Theorem	e23an 38004	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜂   )
Theorem	ee23an 38005	e23an 38004 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))
Theorem	e32 38006	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee32 38007	e32 38006 without virtual deductions. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e32an 38008	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee32an 38009	e33an 37983 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e123 38010	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜒   ,   𝜏   ▶   𝜂   )    &   ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜒   ,   𝜏   ▶   𝜁   )
Theorem	ee123 38011	e123 38010 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂)))    &   ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜁)))
Theorem	el123 38012	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜒   ▶   𝜃   )    &   ⊢ (   𝜏   ▶   𝜂   )    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ (   (   𝜑   ,   𝜒   ,   𝜏   )   ▶   𝜁   )
Theorem	e233 38013	A virtual deduction elimination rule. (Contributed by Alan Sare, 29-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜂   )    &   ⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜁   )
Theorem	e323 38014	A virtual deduction elimination rule. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )    &   ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜁   )
Theorem	e000 38015	A virtual deduction elimination rule. The non-virtual deduction form of e000 38015 is the virtual deduction form. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ 𝜃
Theorem	e00 38016	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 38017	Elimination rule identical to mp2an 704. The non-virtual deduction form is the virtual deduction form, which is mp2an 704. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	eel00cT 38018	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (⊤ → 𝜒)
Theorem	eelTT 38019	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (⊤ → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	e0a 38020	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 38021	An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	eel0cT 38022	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (⊤ → 𝜓)
Theorem	eelT0 38023	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	e0bi 38024	Elimination rule identical to mpbi 219. The non-virtual deduction form is the virtual deduction form, which is mpbi 219. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ 𝜓
Theorem	e0bir 38025	Elimination rule identical to mpbir 220. The non-virtual deduction form is the virtual deduction form, which is mpbir 220. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 ↔ 𝜑)    ⇒   ⊢ 𝜓
Theorem	uun0.1 38026	Convention notation form of un0.1 38027. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ ((⊤ ∧ 𝜓) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	un0.1 38027	⊤ is the constant true, a tautology (see df-tru 1478). 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 38028	A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) Proof was revised to accomodate a possible future version of df-tru 1478. (Revised by David A. Wheeler, 8-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((⊤ ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	uunT1p1 38029	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 38030	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 38031	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 38032	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 38033	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 38034	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 38035	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 858. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜓 ∧ 𝜑) ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
Theorem	un10 38036	A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   (   𝜑   ,   ⊤   )   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ▶   𝜓   )
Theorem	un01 38037	A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   (   ⊤   ,   𝜑   )   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ▶   𝜓   )
Theorem	un2122 38038	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 38039	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 38040	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 38041	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 38042	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 38043	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 38044	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 38045	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 38046	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 38047	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 38048	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 38049	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 38050	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 38051	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 38052	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 38053	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 38054	A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1375 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 38055	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 38056	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 38057	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 38058	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 38059	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 38060	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 38061	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 38062	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 38063	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 38064	A deduction unionizing a non-unionized collection of virtual hypotheses. Commuted version of 3impdir 1374. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜒 ∧ 𝜓) ∧ (𝜑 ∧ 𝜓)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)
Theorem	3impcombi 38065	A 1-hypothesis propositional calculus deduction. (Contributed by Alan Sare, 25-Sep-2017.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
Theorem	3imp231 38066	Importation inference. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)
21.30.6  Theorems proved using Virtual Deduction
Theorem	trsspwALT 38067	Virtual deduction proof of the left-to-right implication of dftr4 4685. A transitive class is a subset of its power class. This proof corresponds to the virtual deduction proof of dftr4 4685 without accumulating results. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴)
Theorem	trsspwALT2 38068	Virtual deduction proof of trsspwALT 38067. This proof is the same as the proof of trsspwALT 38067 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 38069	Short predicate calculus proof of the left-to-right implication of dftr4 4685. 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 38068, which is the virtual deduction proof trsspwALT 38067 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴)
Theorem	sspwtr 38070	Virtual deduction proof of the right-to-left implication of dftr4 4685. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 38070 without accumulating results. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴)
Theorem	sspwtrALT 38071	Virtual deduction proof of sspwtr 38070. This proof is the same as the proof of sspwtr 38070 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	csbabgOLD 38072*	Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) Obsolete as of 19-Aug-2018. Use csbab 3960 instead. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑})
Theorem	csbunigOLD 38073	Distribute proper substitution through the union of a class. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 22-Aug-2018. Use csbuni 4402 instead. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌∪ 𝐵 = ∪ ⦋𝐴 / 𝑥⦌𝐵)
Theorem	csbfv12gALTOLD 38074	Move class substitution in and out of a function value. The proof is derived from the virtual deduction proof csbfv12gALTVD 38157. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 20-Aug-2018. Use csbfv12 6141 instead. (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵))
Theorem	csbxpgOLD 38075	Distribute proper substitution through the Cartesian product of two classes. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018. Use csbrn 5514 instead. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝐷 → ⦋𝐴 / 𝑥⦌(𝐵 × 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 × ⦋𝐴 / 𝑥⦌𝐶))
Theorem	csbingOLD 38076	Distribute proper substitution through an intersection relation. (Contributed by Alan Sare, 22-Jul-2012.) Obsolete as of 18-Aug-2018. Use csbin 3962 instead. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝐵 → ⦋𝐴 / 𝑥⦌(𝐶 ∩ 𝐷) = (⦋𝐴 / 𝑥⦌𝐶 ∩ ⦋𝐴 / 𝑥⦌𝐷))
Theorem	csbresgOLD 38077	Distribute proper substitution through the restriction of a class. csbresgOLD 38077 is derived from the virtual deduction proof csbresgVD 38153. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018. Use csbres 5320 instead. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ↾ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ↾ ⦋𝐴 / 𝑥⦌𝐶))
Theorem	csbrngOLD 38078	Distribute proper substitution through the range of a class. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 23-Aug-2018. Use csbrn 5514 instead. (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌ran 𝐵 = ran ⦋𝐴 / 𝑥⦌𝐵)
Theorem	csbima12gALTOLD 38079	Move class substitution in and out of the image of a function. The proof is derived from the virtual deduction proof csbima12gALTVD 38155. (Contributed by Alan Sare, 10-Nov-2012.) Obsolete as of 20-Aug-2018. Use csbfv12 6141 instead. (Proof modification is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵))
Theorem	sspwtrALT2 38080	Short predicate calculus proof of the right-to-left implication of dftr4 4685. 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 38071, which is the virtual deduction proof sspwtr 38070 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴)
Theorem	pwtrVD 38081	Virtual deduction proof of pwtr 4848; see pwtrrVD 38082 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Tr 𝐴 → Tr 𝒫 𝐴)
Theorem	pwtrrVD 38082	Virtual deduction proof of pwtr 4848; see pwtrVD 38081 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Tr 𝒫 𝐴 → Tr 𝐴)
Theorem	suctrALT 38083	The successor of a transitive class is transitive. The proof of http://us.metamath.org/other/completeusersproof/suctrvd.html is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctrALT 38083 using completeusersproof, which is verified by the Metamath program. The proof of http://us.metamath.org/other/completeusersproof/suctrro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. See suctr 5725 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 38084	Virtual deduction proof of snssiALT 38085. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
Theorem	snssiALT 38085	If a class is an element of another class, then its singleton is a subclass of that other class. Alternate proof of snssi 4280. This theorem was automatically generated from snssiALTVD 38084 using a translation program. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
Theorem	snsslVD 38086	Virtual deduction proof of snssl 38087. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ({𝐴} ⊆ 𝐵 → 𝐴 ∈ 𝐵)
Theorem	snssl 38087	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 4259. The proof of this theorem was automatically generated from snsslVD 38086 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 38088	Virtual deduction proof of snelpwi 4839. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)
Theorem	unipwrVD 38089	Virtual deduction proof of unipwr 38090. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ⊆ ∪ 𝒫 𝐴
Theorem	unipwr 38090	A class is a subclass of the union of its power class. This theorem is the right-to-left subclass lemma of unipw 4845. The proof of this theorem was automatically generated from unipwrVD 38089 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 38091	Virtual deduction proof of sstrALT2 38092. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
Theorem	sstrALT2 38092	Virtual deduction proof of sstr 3576, transitivity of subclasses, Theorem 6 of [Suppes] p. 23. This theorem was automatically generated from sstrALT2VD 38091 using the command file translatewithout_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 38093	Virtual deduction proof of suctrALT2 38094. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Tr 𝐴 → Tr suc 𝐴)
Theorem	suctrALT2 38094	Virtual deduction proof of suctr 5725. The sucessor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD 38093 using the tools command file translatewithout_overwritingminimize_excludingduplicates.cmd . (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Tr 𝐴 → Tr suc 𝐴)
Theorem	elex2VD 38095*	Virtual deduction proof of elex2 3189. (Contributed by Alan Sare, 25-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)
Theorem	elex22VD 38096*	Virtual deduction proof of elex22 3190. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
Theorem	eqsbc3rVD 38097*	Virtual deduction proof of eqsbc3r 3459. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴))
Theorem	zfregs2VD 38098*	Virtual deduction proof of zfregs2 8492. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ≠ ∅ → ¬ ∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥))
Theorem	tpid3gVD 38099	Virtual deduction proof of tpid3g 4248. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴})
Theorem	en3lplem1VD 38100*	Virtual deduction proof of en3lplem1 8394. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)))