P. 371 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37001-37100   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	wvhc3 37001	Syntax for a 3-element virtual hypotheses collection. (Contributed by Alan Sare, 13-Jun-2015.) (New usage is discouraged.)
wff (. ph ,. ps ,. ch ).
Definition	df-vhc3 37002	Definition of a 3-element virtual hypotheses collection. (Contributed by Alan Sare, 13-Jun-2015.) (New usage is discouraged.)
|- ( (. ph ,. ps ,. ch ). <-> ( ph /\ ps /\ ch ) )
Definition	df-vd3 37003	Definition of a 3-hypothesis virtual deduction. (Contributed by Alan Sare, 14-Nov-2011.) (New usage is discouraged.)
|- ( (. ph ,. ps ,. ch ->. th ). <-> ( ( ph /\ ps /\ ch ) -> th ) )
Theorem	dfvd3 37004	Definition of a 3-hypothesis virtual deduction. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( (. ph ,. ps ,. ch ->. th ). <-> ( ph -> ( ps -> ( ch -> th ) ) ) )
Theorem	dfvd3i 37005	Inference form of dfvd3 37004. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ch ->. th ).   =>    |- ( ph -> ( ps -> ( ch -> th ) ) )
Theorem	dfvd3ir 37006	Right-to-left inference form of dfvd3 37004. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- (. ph ,. ps ,. ch ->. th ).
Theorem	dfvd3an 37007	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.)
|- ( (. (. ph ,. ps ,. ch ). ->. th ). <-> ( ( ph /\ ps /\ ch ) -> th ) )
Theorem	dfvd3ani 37008	Inference form of dfvd3an 37007. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. (. ph ,. ps ,. ch ). ->. th ).   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	dfvd3anir 37009	Right-to-left inference form of dfvd3an 37007. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ph /\ ps /\ ch ) -> th )   =>    |- (. (. ph ,. ps ,. ch ). ->. th ).
Syntax	wvhc4 37010	Syntax for a 4-element virtual hypotheses collection. (Contributed by Alan Sare, 17-Oct-2017.) (New usage is discouraged.)
wff (. ph ,. ps ,. ch ,. th ).
Syntax	wvhc5 37011	Syntax for a 5-element virtual hypotheses collection. (Contributed by Alan Sare, 17-Oct-2017.) (New usage is discouraged.)
wff (. ph ,. ps ,. ch ,. th ,. ta ).
Syntax	wvhc6 37012	Syntax for a 6-element virtual hypotheses collection. (Contributed by Alan Sare, 17-Oct-2017.) (New usage is discouraged.)
wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ).
Syntax	wvhc7 37013	Syntax for a 7-element virtual hypotheses collection. (Contributed by Alan Sare, 17-Oct-2017.) (New usage is discouraged.)
wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ).
Syntax	wvhc8 37014	Syntax for an 8-element virtual hypotheses collection. (Contributed by Alan Sare, 17-Oct-2017.) (New usage is discouraged.)
wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ).
Syntax	wvhc9 37015	Syntax for a 9-element virtual hypotheses collection. (Contributed by Alan Sare, 17-Oct-2017.) (New usage is discouraged.)
wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ,. rh ).
Syntax	wvhc10 37016	Syntax for a 10-element virtual hypotheses collection. (Contributed by Alan Sare, 17-Oct-2017.) (New usage is discouraged.)
wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ,. rh ,. mu ).
Syntax	wvhc11 37017	Syntax for an 11-element virtual hypotheses collection. (Contributed by Alan Sare, 17-Oct-2017.) (New usage is discouraged.)
wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ,. rh ,. mu ,. la ).
Syntax	wvhc12 37018	Syntax for a 12-element virtual hypotheses collection. (Contributed by Alan Sare, 17-Oct-2017.) (New usage is discouraged.)
wff (. ph ,. ps ,. ch ,. th ,. ta ,. et ,. ze ,. si ,. rh ,. mu ,. la ,. ka ).
Theorem	vd01 37019	A virtual hypothesis virtually infers a theorem. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   =>    |- (. ps ->. ph ).
Theorem	vd02 37020	Two virtual hypotheses virtually infer a theorem. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   =>    |- (. ps ,. ch ->. ph ).
Theorem	vd03 37021	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.)
|- ph   =>    |- (. ps ,. ch ,. th ->. ph ).
Theorem	vd12 37022	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.)
|- (. ph ->. ps ).   =>    |- (. ph ,. ch ->. ps ).
Theorem	vd13 37023	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.)
|- (. ph ->. ps ).   =>    |- (. ph ,. ch ,. th ->. ps ).
Theorem	vd23 37024	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.)
|- (. ph ,. ps ->. ch ).   =>    |- (. ph ,. ps ,. th ->. ch ).
Theorem	dfvd2imp 37025	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.)
|- ( (. ph ,. ps ->. ch ). -> ( ph -> ( ps -> ch ) ) )
Theorem	dfvd2impr 37026	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.)
|- ( ( ph -> ( ps -> ch ) ) -> (. ph ,. ps ->. ch ). )
Theorem	in2 37027	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.)
|- (. ph ,. ps ->. ch ).   =>    |- (. ph ->. ( ps -> ch ) ).
Theorem	int2 37028	The virtual deduction introduction rule of converting the end virtual hypothesis of 2 virtual hypotheses into an antecedent. Conventional form of int2 37028 is ex 440. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. (. ph ,. ps ). ->. ch ).   =>    |- (. ph ->. ( ps -> ch ) ).
Theorem	iin2 37029	in2 37027 without virtual deductions. (Contributed by Alan Sare, 20-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> ch ) )
Theorem	in2an 37030	The virtual deduction introduction rule converting the second conjunct of the second virtual hypothesis into the antecedent of the conclusion. expd 442 is the non-virtual deduction form of in2an 37030. (Contributed by Alan Sare, 30-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ( ps /\ ch ) ->. th ).   =>    |- (. ph ,. ps ->. ( ch -> th ) ).
Theorem	in3 37031	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.)
|- (. ph ,. ps ,. ch ->. th ).   =>    |- (. ph ,. ps ->. ( ch -> th ) ).
Theorem	iin3 37032	in3 37031 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.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- ( ph -> ( ps -> ( ch -> th ) ) )
Theorem	in3an 37033	The virtual deduction introduction rule converting the second conjunct of the third virtual hypothesis into the antecedent of the conclusion. exp4a 615 is the non-virtual deduction form of in3an 37033. (Contributed by Alan Sare, 25-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ( ch /\ th ) ->. ta ).   =>    |- (. ph ,. ps ,. ch ->. ( th -> ta ) ).
Theorem	int3 37034	The virtual deduction introduction rule of converting the end virtual hypothesis of 3 virtual hypotheses into an antecedent. Conventional form of int3 37034 is 3expia 1217. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. (. ph ,. ps ,. ch ). ->. th ).   =>    |- (. (. ph ,. ps ). ->. ( ch -> th ) ).
Theorem	idn2 37035	Virtual deduction identity rule which is idd 25 with virtual deduction symbols. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ps ).
Theorem	iden2 37036	Virtual deduction identity rule. simpr 467 in conjunction form Virtual Deduction notation. (Contributed by Alan Sare, 5-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. (. ph ,. ps ). ->. ps ).
Theorem	idn3 37037	Virtual deduction identity rule for three virtual hypotheses. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ch ->. ch ).
Theorem	gen11 37038*	Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1784 is gen11 37038 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   =>    |- (. ph ->. A. x ps ).
Theorem	gen11nv 37039	Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis without distinct variables. alrimih 1704 is gen11nv 37039 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   &    |- (. ph ->. ps ).   =>    |- (. ph ->. A. x ps ).
Theorem	gen12 37040*	Virtual deduction generalizing rule for two quantifying variables and one virtual hypothesis. gen12 37040 is alrimivv 1785 with virtual deductions. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   =>    |- (. ph ->. A. x A. y ps ).
Theorem	gen21 37041*	Virtual deduction generalizing rule for one quantifying variables and two virtual hypothesis. gen21 37041 is alrimdv 1786 with virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   =>    |- (. ph ,. ps ->. A. x ch ).
Theorem	gen21nv 37042	Virtual deduction form of alrimdh 1734. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. x ps )   &    |- (. ph ,. ps ->. ch ).   =>    |- (. ph ,. ps ->. A. x ch ).
Theorem	gen31 37043*	Virtual deduction generalizing rule for one quantifying variable and three virtual hypothesis. gen31 37043 is ggen31 36955 with virtual deductions. (Contributed by Alan Sare, 22-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ch ->. th ).   =>    |- (. ph ,. ps ,. ch ->. A. x th ).
Theorem	gen22 37044*	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.)
|- (. ph ,. ps ->. ch ).   =>    |- (. ph ,. ps ->. A. x A. y ch ).
Theorem	ggen22 37045*	gen22 37044 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> A. x A. y ch ) )
Theorem	exinst 37046	Existential Instantiation. Virtual deduction form of exlimexi 36925. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ps -> A. x ps )   &    |- (. E. x ph ,. ph ->. ps ).   =>    |- ( E. x ph -> ps )
Theorem	exinst01 37047	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 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.)
|- E. x ps   &    |- (. ph ,. ps ->. ch ).   &    |- ( ph -> A. x ph )   &    |- ( ch -> A. x ch )   =>    |- (. ph ->. ch ).
Theorem	exinst11 37048	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 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.)
|- (. ph ->. E. x ps ).   &    |- (. ph ,. ps ->. ch ).   &    |- ( ph -> A. x ph )   &    |- ( ch -> A. x ch )   =>    |- (. ph ->. ch ).
Theorem	e1a 37049	A Virtual deduction elimination rule. syl 17 is e1a 37049 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- ( ps -> ch )   =>    |- (. ph ->. ch ).
Theorem	el1 37050	A Virtual deduction elimination rule. syl 17 is el1 37050 without virtual deductions. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- ( ps -> ch )   =>    |- (. ph ->. ch ).
Theorem	e1bi 37051	Biconditional form of e1a 37049. sylib 201 is e1bi 37051 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- ( ps <-> ch )   =>    |- (. ph ->. ch ).
Theorem	e1bir 37052	Right biconditional form of e1a 37049. sylibr 217 is e1bir 37052 without virtual deductions. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- ( ch <-> ps )   =>    |- (. ph ->. ch ).
Theorem	e2 37053	A virtual deduction elimination rule. syl6 34 is e2 37053 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- ( ch -> th )   =>    |- (. ph ,. ps ->. th ).
Theorem	e2bi 37054	Biconditional form of e2 37053. syl6ib 234 is e2bi 37054 without virtual deductions. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- ( ch <-> th )   =>    |- (. ph ,. ps ->. th ).
Theorem	e2bir 37055	Right biconditional form of e2 37053. syl6ibr 235 is e2bir 37055 without virtual deductions. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- ( th <-> ch )   =>    |- (. ph ,. ps ->. th ).
Theorem	ee223 37056	e223 37057 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> th ) )   &    |- ( ph -> ( ps -> ( ta -> et ) ) )   &    |- ( ch -> ( th -> ( et -> ze ) ) )   =>    |- ( ph -> ( ps -> ( ta -> ze ) ) )
Theorem	e223 37057	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- (. ph ,. ps ->. th ).   &    |- (. ph ,. ps ,. ta ->. et ).   &    |- ( ch -> ( th -> ( et -> ze ) ) )   =>    |- (. ph ,. ps ,. ta ->. ze ).
Theorem	e222 37058	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- (. ph ,. ps ->. th ).   &    |- (. ph ,. ps ->. ta ).   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- (. ph ,. ps ->. et ).
Theorem	e220 37059	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- (. ph ,. ps ->. th ).   &    |- ta   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- (. ph ,. ps ->. et ).
Theorem	ee220 37060	e220 37059 without virtual deductions. (Contributed by Alan Sare, 12-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> th ) )   &    |- ta   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- ( ph -> ( ps -> et ) )
Theorem	e202 37061	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- th   &    |- (. ph ,. ps ->. ta ).   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- (. ph ,. ps ->. et ).
Theorem	ee202 37062	e202 37061 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   &    |- th   &    |- ( ph -> ( ps -> ta ) )   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- ( ph -> ( ps -> et ) )
Theorem	e022 37063	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- (. ps ,. ch ->. th ).   &    |- (. ps ,. ch ->. ta ).   &    |- ( ph -> ( th -> ( ta -> et ) ) )   =>    |- (. ps ,. ch ->. et ).
Theorem	ee022 37064	e022 37063 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ps -> ( ch -> th ) )   &    |- ( ps -> ( ch -> ta ) )   &    |- ( ph -> ( th -> ( ta -> et ) ) )   =>    |- ( ps -> ( ch -> et ) )
Theorem	e002 37065	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ps   &    |- (. ch ,. th ->. ta ).   &    |- ( ph -> ( ps -> ( ta -> et ) ) )   =>    |- (. ch ,. th ->. et ).
Theorem	ee002 37066	e002 37065 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ps   &    |- ( ch -> ( th -> ta ) )   &    |- ( ph -> ( ps -> ( ta -> et ) ) )   =>    |- ( ch -> ( th -> et ) )
Theorem	e020 37067	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- (. ps ,. ch ->. th ).   &    |- ta   &    |- ( ph -> ( th -> ( ta -> et ) ) )   =>    |- (. ps ,. ch ->. et ).
Theorem	ee020 37068	e020 37067 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ps -> ( ch -> th ) )   &    |- ta   &    |- ( ph -> ( th -> ( ta -> et ) ) )   =>    |- ( ps -> ( ch -> et ) )
Theorem	e200 37069	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- th   &    |- ta   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- (. ph ,. ps ->. et ).
Theorem	ee200 37070	e200 37069 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   &    |- th   &    |- ta   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- ( ph -> ( ps -> et ) )
Theorem	e221 37071	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- (. ph ,. ps ->. th ).   &    |- (. ph ->. ta ).   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- (. ph ,. ps ->. et ).
Theorem	ee221 37072	e221 37071 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> th ) )   &    |- ( ph -> ta )   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- ( ph -> ( ps -> et ) )
Theorem	e212 37073	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- (. ph ->. th ).   &    |- (. ph ,. ps ->. ta ).   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- (. ph ,. ps ->. et ).
Theorem	ee212 37074	e212 37073 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> th )   &    |- ( ph -> ( ps -> ta ) )   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- ( ph -> ( ps -> et ) )
Theorem	e122 37075	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ph ,. ch ->. th ).   &    |- (. ph ,. ch ->. ta ).   &    |- ( ps -> ( th -> ( ta -> et ) ) )   =>    |- (. ph ,. ch ->. et ).
Theorem	e112 37076	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ph ->. ch ).   &    |- (. ph ,. th ->. ta ).   &    |- ( ps -> ( ch -> ( ta -> et ) ) )   =>    |- (. ph ,. th ->. et ).
Theorem	ee112 37077	e112 37076 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> ( th -> ta ) )   &    |- ( ps -> ( ch -> ( ta -> et ) ) )   =>    |- ( ph -> ( th -> et ) )
Theorem	e121 37078	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ph ,. ch ->. th ).   &    |- (. ph ->. ta ).   &    |- ( ps -> ( th -> ( ta -> et ) ) )   =>    |- (. ph ,. ch ->. et ).
Theorem	e211 37079	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- (. ph ->. th ).   &    |- (. ph ->. ta ).   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- (. ph ,. ps ->. et ).
Theorem	ee211 37080	e211 37079 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- ( ph -> ( ps -> et ) )
Theorem	e210 37081	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- (. ph ->. th ).   &    |- ta   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- (. ph ,. ps ->. et ).
Theorem	ee210 37082	e210 37081 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> th )   &    |- ta   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- ( ph -> ( ps -> et ) )
Theorem	e201 37083	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- th   &    |- (. ph ->. ta ).   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- (. ph ,. ps ->. et ).
Theorem	ee201 37084	e201 37083 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   &    |- th   &    |- ( ph -> ta )   &    |- ( ch -> ( th -> ( ta -> et ) ) )   =>    |- ( ph -> ( ps -> et ) )
Theorem	e120 37085	A virtual deduction elimination rule. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ph ,. ch ->. th ).   &    |- ta   &    |- ( ps -> ( th -> ( ta -> et ) ) )   =>    |- (. ph ,. ch ->. et ).
Theorem	ee120 37086	Virtual deduction rule e120 37085 without virtual deduction symbols. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ps )   &    |- ( ph -> ( ch -> th ) )   &    |- ta   &    |- ( ps -> ( th -> ( ta -> et ) ) )   =>    |- ( ph -> ( ch -> et ) )
Theorem	e021 37087	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- (. ps ,. ch ->. th ).   &    |- (. ps ->. ta ).   &    |- ( ph -> ( th -> ( ta -> et ) ) )   =>    |- (. ps ,. ch ->. et ).
Theorem	ee021 37088	e021 37087 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ps -> ( ch -> th ) )   &    |- ( ps -> ta )   &    |- ( ph -> ( th -> ( ta -> et ) ) )   =>    |- ( ps -> ( ch -> et ) )
Theorem	e012 37089	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- (. ps ->. ch ).   &    |- (. ps ,. th ->. ta ).   &    |- ( ph -> ( ch -> ( ta -> et ) ) )   =>    |- (. ps ,. th ->. et ).
Theorem	ee012 37090	e012 37089 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ps -> ch )   &    |- ( ps -> ( th -> ta ) )   &    |- ( ph -> ( ch -> ( ta -> et ) ) )   =>    |- ( ps -> ( th -> et ) )
Theorem	e102 37091	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- ch   &    |- (. ph ,. th ->. ta ).   &    |- ( ps -> ( ch -> ( ta -> et ) ) )   =>    |- (. ph ,. th ->. et ).
Theorem	ee102 37092	e102 37091 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ps )   &    |- ch   &    |- ( ph -> ( th -> ta ) )   &    |- ( ps -> ( ch -> ( ta -> et ) ) )   =>    |- ( ph -> ( th -> et ) )
Theorem	e22 37093	A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- (. ph ,. ps ->. th ).   &    |- ( ch -> ( th -> ta ) )   =>    |- (. ph ,. ps ->. ta ).
Theorem	e22an 37094	Conjunction form of e22 37093. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- (. ph ,. ps ->. th ).   &    |- ( ( ch /\ th ) -> ta )   =>    |- (. ph ,. ps ->. ta ).
Theorem	ee22an 37095	e22an 37094 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> th ) )   &    |- ( ( ch /\ th ) -> ta )   =>    |- ( ph -> ( ps -> ta ) )
Theorem	e111 37096	A virtual deduction elimination rule (see syl3c 63). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ph ->. ch ).   &    |- (. ph ->. th ).   &    |- ( ps -> ( ch -> ( th -> ta ) ) )   =>    |- (. ph ->. ta ).
Theorem	e1111 37097	A virtual deduction elimination rule. (Contributed by Alan Sare, 6-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ph ->. ch ).   &    |- (. ph ->. th ).   &    |- (. ph ->. ta ).   &    |- ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) )   =>    |- (. ph ->. et ).
Theorem	e110 37098	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ph ->. ch ).   &    |- th   &    |- ( ps -> ( ch -> ( th -> ta ) ) )   =>    |- (. ph ->. ta ).
Theorem	ee110 37099	e110 37098 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- th   &    |- ( ps -> ( ch -> ( th -> ta ) ) )   =>    |- ( ph -> ta )
Theorem	e101 37100	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- ch   &    |- (. ph ->. th ).   &    |- ( ps -> ( ch -> ( th -> ta ) ) )   =>    |- (. ph ->. ta ).