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	e110 44701	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee110 44702	e110 44701 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e101 44703	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee101 44704	e101 44703 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e011 44705	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (   𝜓   ▶   𝜃   )    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜓   ▶   𝜏   )
Theorem	ee011 44706	e011 44705 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	e100 44707	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee100 44708	e100 44707 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e010 44709	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜓   ▶   𝜏   )
Theorem	ee010 44710	e010 44709 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ 𝜃    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	e001 44711	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (   𝜒   ▶   𝜃   )    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜒   ▶   𝜏   )
Theorem	ee001 44712	e001 44711 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	e11 44713	A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ (𝜓 → (𝜒 → 𝜃))    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	e11an 44714	Conjunction form of e11 44713. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	ee11an 44715	e11an 44714 without virtual deductions. syl22anc 838 is also e11an 44714 without virtual deductions, exept with a different order of hypotheses. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	e01 44716	A virtual deduction elimination rule. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (𝜑 → (𝜒 → 𝜃))    ⇒   ⊢ (   𝜓   ▶   𝜃   )
Theorem	e01an 44717	Conjunction form of e01 44716. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   𝜓   ▶   𝜃   )
Theorem	ee01an 44718	e01an 44717 without virtual deductions. sylancr 587 is also a form of e01an 44717 without virtual deduction, except the order of the hypotheses is different. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	e10 44719	A virtual deduction elimination rule (see mpisyl 21). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ (𝜓 → (𝜒 → 𝜃))    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	e10an 44720	Conjunction form of e10 44719. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	ee10an 44721	e10an 44720 without virtual deductions. sylancl 586 is also e10an 44720 without virtual deductions, except the order of the hypotheses is different. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	e02 44722	A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜑 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	e02an 44723	Conjunction form of e02 44722. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	ee02an 44724	e02an 44723 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜓 → (𝜒 → 𝜏))
Theorem	eel021old 44725	el021old 44726 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜏)
Theorem	el021old 44726	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   (   𝜓   ,   𝜒   )   ▶   𝜃   )    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   (   𝜓   ,   𝜒   )   ▶   𝜏   )
Theorem	eel000cT 44727	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (⊤ → 𝜃)
Theorem	eel0TT 44728	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (⊤ → 𝜓)    &   ⊢ (⊤ → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	eelT00 44729	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	eelTTT 44730	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (⊤ → 𝜓)    &   ⊢ (⊤ → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	eelT11 44731	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	eelT1 44732	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Alan Sare, 23-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	eelT12 44733	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜃 → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜓 ∧ 𝜃) → 𝜂)
Theorem	eelTT1 44734	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (⊤ → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	eelT01 44735	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	eel0T1 44736	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (⊤ → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	eel12131 44737	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	eel2131 44738	syl2an 596 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜂)
Theorem	eel3132 44739	syl2an 596 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜂)
Theorem	eel0321old 44740	el0321old 44741 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜂)
Theorem	el0321old 44741	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   (   𝜓   ,   𝜒   ,   𝜃   )   ▶   𝜏   )    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   (   𝜓   ,   𝜒   ,   𝜃   )   ▶   𝜂   )
Theorem	eel2122old 44742	el2122old 44743 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ (𝜓 → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜂)
Theorem	el2122old 44743	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   (   𝜑   ,   𝜓   )   ▶   𝜒   )    &   ⊢ (   𝜓   ▶   𝜃   )    &   ⊢ (   𝜓   ▶   𝜏   )    &   ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   (   𝜑   ,   𝜓   )   ▶   𝜂   )
Theorem	eel0000 44744	Elimination rule similar to mp4an 693, except with a left-nested conjunction unification theorem. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ 𝜏
Theorem	eel00001 44745	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜏 → 𝜂)    &   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜏 → 𝜁)
Theorem	eel00000 44746	Elimination rule similar eel0000 44744, except with five hpothesis steps. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ 𝜏    &   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ 𝜂
Theorem	eel11111 44747	Five-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc 1384 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	e12 44748	A virtual deduction elimination rule (see sylsyld 61). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )
Theorem	e12an 44749	Conjunction form of e12 44748 (see syl6an 684). (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )
Theorem	el12 44750	Virtual deduction form of syl2an 596. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜏   ▶   𝜒   )    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   (   𝜑   ,   𝜏   )   ▶   𝜃   )
Theorem	e20 44751	A virtual deduction elimination rule (see syl6mpi 67). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (𝜒 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	e20an 44752	Conjunction form of e20 44751. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	ee20an 44753	e20an 44752 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜃    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜏))
Theorem	e21 44754	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 44755	Conjunction form of e21 44754. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	ee21an 44756	e21an 44755 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜏))
Theorem	e333 44757	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )    &   ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜁   )
Theorem	e33 44758	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	e33an 44759	Conjunction form of e33 44758. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee33an 44760	e33an 44759 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e3 44761	Meta-connective form of syl8 76. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	e3bi 44762	Biconditional form of e3 44761. syl8ib 256 is e3bi 44762 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜃 ↔ 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	e3bir 44763	Right biconditional form of e3 44761. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜏 ↔ 𝜃)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	e03 44764	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜓   ,   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	ee03 44765	e03 44764 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    &   ⊢ (𝜑 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂)))
Theorem	e03an 44766	Conjunction form of e03 44764. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜓   ,   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	ee03an 44767	Conjunction form of ee03 44765. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂)))
Theorem	e30 44768	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee30 44769	e30 44768 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ 𝜏    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e30an 44770	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee30an 44771	Conjunction form of ee30 44769. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ 𝜏    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e13 44772	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	e13an 44773	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ ((𝜓 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	ee13an 44774	e13an 44773 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    &   ⊢ ((𝜓 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂)))
Theorem	e31 44775	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee31 44776	e31 44775 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e31an 44777	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee31an 44778	e31an 44777 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e23 44779	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 44780	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜂   )
Theorem	ee23an 44781	e23an 44780 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))
Theorem	e32 44782	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee32 44783	e32 44782 without virtual deductions. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e32an 44784	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee32an 44785	e33an 44759 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e123 44786	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜒   ,   𝜏   ▶   𝜂   )    &   ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜒   ,   𝜏   ▶   𝜁   )
Theorem	ee123 44787	e123 44786 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂)))    &   ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜁)))
Theorem	el123 44788	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜒   ▶   𝜃   )    &   ⊢ (   𝜏   ▶   𝜂   )    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ (   (   𝜑   ,   𝜒   ,   𝜏   )   ▶   𝜁   )
Theorem	e233 44789	A virtual deduction elimination rule. (Contributed by Alan Sare, 29-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜂   )    &   ⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜁   )
Theorem	e323 44790	A virtual deduction elimination rule. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )    &   ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜁   )
Theorem	e000 44791	A virtual deduction elimination rule. The non-virtual deduction form of e000 44791 is the virtual deduction form. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ 𝜃
Theorem	e00 44792	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 44793	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 44794	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (⊤ → 𝜒)
Theorem	eelTT 44795	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (⊤ → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	e0a 44796	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 44797	An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	eel0cT 44798	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (⊤ → 𝜓)
Theorem	eelT0 44799	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒
Theorem	e0bi 44800	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.)
⊢ 𝜑    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ 𝜓