P. 448 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44701-44800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	e20an 44701	Conjunction form of e20 44700. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	ee20an 44702	e20an 44701 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜃    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜏))
Theorem	e21 44703	A virtual deduction elimination rule (see syl6ci 71). (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (𝜒 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	e21an 44704	Conjunction form of e21 44703. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	ee21an 44705	e21an 44704 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜏))
Theorem	e333 44706	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )    &   ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜁   )
Theorem	e33 44707	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	e33an 44708	Conjunction form of e33 44707. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee33an 44709	e33an 44708 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e3 44710	Meta-connective form of syl8 76. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	e3bi 44711	Biconditional form of e3 44710. syl8ib 256 is e3bi 44711 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜃 ↔ 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	e3bir 44712	Right biconditional form of e3 44710. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜏 ↔ 𝜃)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	e03 44713	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜓   ,   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	ee03 44714	e03 44713 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    &   ⊢ (𝜑 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂)))
Theorem	e03an 44715	Conjunction form of e03 44713. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜓   ,   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	ee03an 44716	Conjunction form of ee03 44714. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂)))
Theorem	e30 44717	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee30 44718	e30 44717 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ 𝜏    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e30an 44719	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee30an 44720	Conjunction form of ee30 44718. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ 𝜏    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e13 44721	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	e13an 44722	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ ((𝜓 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	ee13an 44723	e13an 44722 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    &   ⊢ ((𝜓 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂)))
Theorem	e31 44724	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee31 44725	e31 44724 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e31an 44726	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee31an 44727	e31an 44726 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e23 44728	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 44729	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜂   )
Theorem	ee23an 44730	e23an 44729 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))
Theorem	e32 44731	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee32 44732	e32 44731 without virtual deductions. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e32an 44733	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee32an 44734	e33an 44708 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e123 44735	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜒   ,   𝜏   ▶   𝜂   )    &   ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜒   ,   𝜏   ▶   𝜁   )
Theorem	ee123 44736	e123 44735 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂)))    &   ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜁)))
Theorem	el123 44737	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜒   ▶   𝜃   )    &   ⊢ (   𝜏   ▶   𝜂   )    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ (   (   𝜑   ,   𝜒   ,   𝜏   )   ▶   𝜁   )
Theorem	e233 44738	A virtual deduction elimination rule. (Contributed by Alan Sare, 29-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜂   )    &   ⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜁   )
Theorem	e323 44739	A virtual deduction elimination rule. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )    &   ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜁   )
Theorem	e000 44740	A virtual deduction elimination rule. The non-virtual deduction form of e000 44740 is the virtual deduction form. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ 𝜃
Theorem	e00 44741	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 44742	Elimination rule identical to mp2an 692. The non-virtual deduction form is the virtual deduction form, which is mp2an 692. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	eel00cT 44743	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (⊤ → 𝜒)
Theorem	eelTT 44744	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (⊤ → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	e0a 44745	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 44746	An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	eel0cT 44747	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (⊤ → 𝜓)
Theorem	eelT0 44748	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	e0bi 44749	Elimination rule identical to mpbi 230. The non-virtual deduction form is the virtual deduction form, which is mpbi 230. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ 𝜓
Theorem	e0bir 44750	Elimination rule identical to mpbir 231. The non-virtual deduction form is the virtual deduction form, which is mpbir 231. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 ↔ 𝜑)    ⇒   ⊢ 𝜓
Theorem	uun0.1 44751	Convention notation form of un0.1 44752. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ ((⊤ ∧ 𝜓) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	un0.1 44752	⊤ is the constant true, a tautology (see df-tru 1543). 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 44753	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 1543. (Revised by David A. Wheeler, 8-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((⊤ ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	uunT1p1 44754	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 44755	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 44756	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 44757	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 44758	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 44759	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 44760	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 673. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜓 ∧ 𝜑) ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
Theorem	un10 44761	A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   (   𝜑   ,   ⊤   )   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ▶   𝜓   )
Theorem	un01 44762	A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   (   ⊤   ,   𝜑   )   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ▶   𝜓   )
Theorem	un2122 44763	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 44764	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 44765	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 44766	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 44767	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 44768	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 44769	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 44770	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 44771	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 44772	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 44773	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 44774	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 44775	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 44776	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 44777	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 44778	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 44779	A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1421 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 44780	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 44781	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 44782	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 44783	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 44784	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 44785	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 44786	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 44787	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 44788	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 44789	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 44790	A 1-hypothesis propositional calculus deduction. (Contributed by Alan Sare, 25-Sep-2017.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
21.41.6  Theorems proved using Virtual Deduction
Theorem	trsspwALT 44791	Virtual deduction proof of the left-to-right implication of dftr4 5208. A transitive class is a subset of its power class. This proof corresponds to the virtual deduction proof of dftr4 5208 without accumulating results. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴)
Theorem	trsspwALT2 44792	Virtual deduction proof of trsspwALT 44791. This proof is the same as the proof of trsspwALT 44791 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 44793	Short predicate calculus proof of the left-to-right implication of dftr4 5208. 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 44792, which is the virtual deduction proof trsspwALT 44791 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴)
Theorem	sspwtr 44794	Virtual deduction proof of the right-to-left implication of dftr4 5208. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 44794 without accumulating results. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴)
Theorem	sspwtrALT 44795	Virtual deduction proof of sspwtr 44794. This proof is the same as the proof of sspwtr 44794 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 44796	Short predicate calculus proof of the right-to-left implication of dftr4 5208. 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 44795, which is the virtual deduction proof sspwtr 44794 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴)
Theorem	pwtrVD 44797	Virtual deduction proof of pwtr 5399; see pwtrrVD 44798 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (Tr 𝐴 → Tr 𝒫 𝐴)
Theorem	pwtrrVD 44798	Virtual deduction proof of pwtr 5399; see pwtrVD 44797 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (Tr 𝒫 𝐴 → Tr 𝐴)
Theorem	suctrALT 44799	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 44799 using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/suctrro.html 44799 is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. See suctr 6399 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 44800	Virtual deduction proof of snssiALT 44801. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)