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	dfvd2anir 44701	Right-to-left inference form of dfvd2an 44699. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (   (   𝜑   ,   𝜓   )   ▶   𝜒   )
Theorem	dfvd2i 44702	Inference form of dfvd2 44696. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	dfvd2ir 44703	Right-to-left inference form of dfvd2 44696. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )
Syntax	wvd3 44704	Syntax for a 3-hypothesis virtual deduction. (New usage is discouraged.)
wff (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )
Syntax	wvhc3 44705	Syntax for a 3-element virtual hypotheses collection. (Contributed by Alan Sare, 13-Jun-2015.) (New usage is discouraged.)
wff (   𝜑   ,   𝜓   ,   𝜒   )
Definition	df-vhc3 44706	Definition of a 3-element virtual hypotheses collection. (Contributed by Alan Sare, 13-Jun-2015.) (New usage is discouraged.)
⊢ ((   𝜑   ,   𝜓   ,   𝜒   ) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
Definition	df-vd3 44707	Definition of a 3-hypothesis virtual deduction. (Contributed by Alan Sare, 14-Nov-2011.) (New usage is discouraged.)
⊢ ((   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   ) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃))
Theorem	dfvd3 44708	Definition of a 3-hypothesis virtual deduction. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   ) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃))))
Theorem	dfvd3i 44709	Inference form of dfvd3 44708. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	dfvd3ir 44710	Right-to-left inference form of dfvd3 44708. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )
Theorem	dfvd3an 44711	Definition of a 3-hypothesis virtual deduction in vd conjunction form. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((   (   𝜑   ,   𝜓   ,   𝜒   )   ▶   𝜃   ) ↔ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃))
Theorem	dfvd3ani 44712	Inference form of dfvd3an 44711. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   (   𝜑   ,   𝜓   ,   𝜒   )   ▶   𝜃   )    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	dfvd3anir 44713	Right-to-left inference form of dfvd3an 44711. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   (   𝜑   ,   𝜓   ,   𝜒   )   ▶   𝜃   )
Theorem	vd01 44714	A virtual hypothesis virtually infers a theorem. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    ⇒   ⊢ (   𝜓   ▶   𝜑   )
Theorem	vd02 44715	Two virtual hypotheses virtually infer a theorem. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜑   )
Theorem	vd03 44716	A theorem is virtually inferred by the 3 virtual hypotheses. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    ⇒   ⊢ (   𝜓   ,   𝜒   ,   𝜃   ▶   𝜑   )
Theorem	vd12 44717	A virtual deduction with 1 virtual hypothesis virtually inferring a virtual conclusion infers that the same conclusion is virtually inferred by the same virtual hypothesis and an additional hypothesis. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜓   )
Theorem	vd13 44718	A virtual deduction with 1 virtual hypothesis virtually inferring a virtual conclusion infers that the same conclusion is virtually inferred by the same virtual hypothesis and a two additional hypotheses. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ,   𝜒   ,   𝜃   ▶   𝜓   )
Theorem	vd23 44719	A virtual deduction with 2 virtual hypotheses virtually inferring a virtual conclusion infers that the same conclusion is virtually inferred by the same 2 virtual hypotheses and a third hypothesis. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜒   )
Theorem	dfvd2imp 44720	The virtual deduction form of a 2-antecedent nested implication implies the 2-antecedent nested implication. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((   𝜑   ,   𝜓   ▶   𝜒   ) → (𝜑 → (𝜓 → 𝜒)))
Theorem	dfvd2impr 44721	A 2-antecedent nested implication implies its virtual deduction form. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (   𝜑   ,   𝜓   ▶   𝜒   ))
Theorem	in2 44722	The virtual deduction introduction rule of converting the end virtual hypothesis of 2 virtual hypotheses into an antecedent. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    ⇒   ⊢ (   𝜑   ▶   (𝜓 → 𝜒)   )
Theorem	int2 44723	The virtual deduction introduction rule of converting the end virtual hypothesis of 2 virtual hypotheses into an antecedent. Conventional form of int2 44723 is ex 412. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   (   𝜑   ,   𝜓   )   ▶   𝜒   )    ⇒   ⊢ (   𝜑   ▶   (𝜓 → 𝜒)   )
Theorem	iin2 44724	in2 44722 without virtual deductions. (Contributed by Alan Sare, 20-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜒))
Theorem	in2an 44725	The virtual deduction introduction rule converting the second conjunct of the second virtual hypothesis into the antecedent of the conclusion. expd 415 is the non-virtual deduction form of in2an 44725. (Contributed by Alan Sare, 30-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   (𝜓 ∧ 𝜒)   ▶   𝜃   )    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   (𝜒 → 𝜃)   )
Theorem	in3 44726	The virtual deduction introduction rule of converting the end virtual hypothesis of 3 virtual hypotheses into an antecedent. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   (𝜒 → 𝜃)   )
Theorem	iin3 44727	in3 44726 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	in3an 44728	The virtual deduction introduction rule converting the second conjunct of the third virtual hypothesis into the antecedent of the conclusion. exp4a 431 is the non-virtual deduction form of in3an 44728. (Contributed by Alan Sare, 25-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   (𝜒 ∧ 𝜃)   ▶   𝜏   )    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   (𝜃 → 𝜏)   )
Theorem	int3 44729	The virtual deduction introduction rule of converting the end virtual hypothesis of 3 virtual hypotheses into an antecedent. Conventional form of int3 44729 is 3expia 1121. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   (   𝜑   ,   𝜓   ,   𝜒   )   ▶   𝜃   )    ⇒   ⊢ (   (   𝜑   ,   𝜓   )   ▶   (𝜒 → 𝜃)   )
Theorem	idn2 44730	Virtual deduction identity rule which is idd 24 with virtual deduction symbols. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜓   )
Theorem	iden2 44731	Virtual deduction identity rule. simpr 484 in conjunction form Virtual Deduction notation. (Contributed by Alan Sare, 5-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   (   𝜑   ,   𝜓   )   ▶   𝜓   )
Theorem	idn3 44732	Virtual deduction identity rule for three virtual hypotheses. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜒   )
Theorem	gen11 44733*	Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1928 is gen11 44733 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ▶   ∀𝑥𝜓   )
Theorem	gen11nv 44734	Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis without distinct variables. alrimih 1825 is gen11nv 44734 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (   𝜑   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ▶   ∀𝑥𝜓   )
Theorem	gen12 44735*	Virtual deduction generalizing rule for two quantifying variables and one virtual hypothesis. gen12 44735 is alrimivv 1929 with virtual deductions. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ▶   ∀𝑥∀𝑦𝜓   )
Theorem	gen21 44736*	Virtual deduction generalizing rule for one quantifying variables and two virtual hypothesis. gen21 44736 is alrimdv 1930 with virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   ∀𝑥𝜒   )
Theorem	gen21nv 44737	Virtual deduction form of alrimdh 1864. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   ∀𝑥𝜒   )
Theorem	gen31 44738*	Virtual deduction generalizing rule for one quantifying variable and three virtual hypothesis. gen31 44738 is ggen31 44662 with virtual deductions. (Contributed by Alan Sare, 22-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   ∀𝑥𝜃   )
Theorem	gen22 44739*	Virtual deduction generalizing rule for two quantifying variables and two virtual hypothesis. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   ∀𝑥∀𝑦𝜒   )
Theorem	ggen22 44740*	gen22 44739 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥∀𝑦𝜒))
Theorem	exinst 44741	Existential Instantiation. Virtual deduction form of exlimexi 44641. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (   ∃𝑥𝜑   ,   𝜑   ▶   𝜓   )    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	exinst01 44742	Existential Instantiation. Virtual Deduction rule corresponding to a special case of the Natural Deduction Sequent Calculus rule called Rule C in [Margaris] p. 79 and E ∃ in Table 1 on page 4 of the paper "Extracting information from intermediate T-systems" (2000) presented at IMLA99 by Mauro Ferrari, Camillo Fiorentini, and Pierangelo Miglioli. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥𝜓    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	exinst11 44743	Existential Instantiation. Virtual Deduction rule corresponding to a special case of the Natural Deduction Sequent Calculus rule called Rule C in [Margaris] p. 79 and E ∃ in Table 1 on page 4 of the paper "Extracting information from intermediate T-systems" (2000) presented at IMLA99 by Mauro Ferrari, Camillo Fiorentini, and Pierangelo Miglioli. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   ∃𝑥𝜓   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	e1a 44744	A Virtual deduction elimination rule. syl 17 is e1a 44744 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	el1 44745	A Virtual deduction elimination rule. syl 17 is el1 44745 without virtual deductions. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	e1bi 44746	Biconditional form of e1a 44744. sylib 218 is e1bi 44746 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	e1bir 44747	Right biconditional form of e1a 44744. sylibr 234 is e1bir 44747 without virtual deductions. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (𝜒 ↔ 𝜓)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	e2 44748	A virtual deduction elimination rule. syl6 35 is e2 44748 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
Theorem	e2bi 44749	Biconditional form of e2 44748. imbitrdi 251 is e2bi 44749 without virtual deductions. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
Theorem	e2bir 44750	Right biconditional form of e2 44748. imbitrrdi 252 is e2bir 44750 without virtual deductions. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (𝜃 ↔ 𝜒)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
Theorem	ee223 44751	e223 44752 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    &   ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜁)))
Theorem	e223 44752	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜏   ▶   𝜂   )    &   ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜏   ▶   𝜁   )
Theorem	e222 44753	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	e220 44754	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee220 44755	e220 44754 without virtual deductions. (Contributed by Alan Sare, 12-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e202 44756	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee202 44757	e202 44756 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜃    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e022 44758	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee022 44759	e022 44758 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ (𝜓 → (𝜒 → 𝜏))    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜒 → 𝜂))
Theorem	e002 44760	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	ee002 44761	e002 44760 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (𝜒 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜒 → (𝜃 → 𝜂))
Theorem	e020 44762	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee020 44763	e020 44762 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ 𝜏    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜒 → 𝜂))
Theorem	e200 44764	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee200 44765	e200 44764 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜃    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e221 44766	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee221 44767	e221 44766 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e212 44768	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee212 44769	e212 44768 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e122 44770	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜂   )
Theorem	e112 44771	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜃   ▶   𝜂   )
Theorem	ee112 44772	e112 44771 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜃 → 𝜂))
Theorem	e121 44773	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜂   )
Theorem	e211 44774	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee211 44775	e211 44774 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e210 44776	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee210 44777	e210 44776 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e201 44778	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee201 44779	e201 44778 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜃    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e120 44780	A virtual deduction elimination rule. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜂   )
Theorem	ee120 44781	Virtual deduction rule e120 44780 without virtual deduction symbols. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ 𝜏    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜂))
Theorem	e021 44782	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜓   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee021 44783	e021 44782 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ (𝜓 → 𝜏)    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜒 → 𝜂))
Theorem	e012 44784	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜃   ▶   𝜂   )
Theorem	ee012 44785	e012 44784 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜃 → 𝜂))
Theorem	e102 44786	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ (   𝜑   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜃   ▶   𝜂   )
Theorem	ee102 44787	e102 44786 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜃 → 𝜂))
Theorem	e22 44788	A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ (𝜒 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	e22an 44789	Conjunction form of e22 44788. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	ee22an 44790	e22an 44789 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜏))
Theorem	e111 44791	A virtual deduction elimination rule (see syl3c 66). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	e1111 44792	A virtual deduction elimination rule. (Contributed by Alan Sare, 6-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))    ⇒   ⊢ (   𝜑   ▶   𝜂   )
Theorem	e110 44793	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee110 44794	e110 44793 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e101 44795	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee101 44796	e101 44795 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e011 44797	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (   𝜓   ▶   𝜃   )    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜓   ▶   𝜏   )
Theorem	ee011 44798	e011 44797 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	e100 44799	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee100 44800	e100 44799 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)