P. 372 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37101-37200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ee101 37101	e101 37100 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ps )   &    |- ch   &    |- ( ph -> th )   &    |- ( ps -> ( ch -> ( th -> ta ) ) )   =>    |- ( ph -> ta )
Theorem	e011 37102	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 ).   &    |- ( ph -> ( ch -> ( th -> ta ) ) )   =>    |- (. ps ->. ta ).
Theorem	ee011 37103	e011 37102 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ps -> ch )   &    |- ( ps -> th )   &    |- ( ph -> ( ch -> ( th -> ta ) ) )   =>    |- ( ps -> ta )
Theorem	e100 37104	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 -> ( th -> ta ) ) )   =>    |- (. ph ->. ta ).
Theorem	ee100 37105	e100 37104 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ps )   &    |- ch   &    |- th   &    |- ( ps -> ( ch -> ( th -> ta ) ) )   =>    |- ( ph -> ta )
Theorem	e010 37106	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 -> ( ch -> ( th -> ta ) ) )   =>    |- (. ps ->. ta ).
Theorem	ee010 37107	e010 37106 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ps -> ch )   &    |- th   &    |- ( ph -> ( ch -> ( th -> ta ) ) )   =>    |- ( ps -> ta )
Theorem	e001 37108	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 -> ( th -> ta ) ) )   =>    |- (. ch ->. ta ).
Theorem	ee001 37109	e001 37108 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ps   &    |- ( ch -> th )   &    |- ( ph -> ( ps -> ( th -> ta ) ) )   =>    |- ( ch -> ta )
Theorem	e11 37110	A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ph ->. ch ).   &    |- ( ps -> ( ch -> th ) )   =>    |- (. ph ->. th ).
Theorem	e11an 37111	Conjunction form of e11 37110. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ph ->. ch ).   &    |- ( ( ps /\ ch ) -> th )   =>    |- (. ph ->. th ).
Theorem	ee11an 37112	e11an 37111 without virtual deductions. syl22anc 1277 is also e11an 37111 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.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	e01 37113	A virtual deduction elimination rule. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- (. ps ->. ch ).   &    |- ( ph -> ( ch -> th ) )   =>    |- (. ps ->. th ).
Theorem	e01an 37114	Conjunction form of e01 37113. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- (. ps ->. ch ).   &    |- ( ( ph /\ ch ) -> th )   =>    |- (. ps ->. th ).
Theorem	ee01an 37115	e01an 37114 without virtual deductions. sylancr 674 is also a form of e01an 37114 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.)
|- ph   &    |- ( ps -> ch )   &    |- ( ( ph /\ ch ) -> th )   =>    |- ( ps -> th )
Theorem	e10 37116	A virtual deduction elimination rule (see mpisyl 21). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- ch   &    |- ( ps -> ( ch -> th ) )   =>    |- (. ph ->. th ).
Theorem	e10an 37117	Conjunction form of e10 37116. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- ch   &    |- ( ( ps /\ ch ) -> th )   =>    |- (. ph ->. th ).
Theorem	ee10an 37118	e10an 37117 without virtual deductions. sylancl 673 is also e10an 37117 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.)
|- ( ph -> ps )   &    |- ch   &    |- ( ( ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	e02 37119	A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- (. ps ,. ch ->. th ).   &    |- ( ph -> ( th -> ta ) )   =>    |- (. ps ,. ch ->. ta ).
Theorem	e02an 37120	Conjunction form of e02 37119. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- (. ps ,. ch ->. th ).   &    |- ( ( ph /\ th ) -> ta )   =>    |- (. ps ,. ch ->. ta ).
Theorem	ee02an 37121	e02an 37120 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ps -> ( ch -> th ) )   &    |- ( ( ph /\ th ) -> ta )   =>    |- ( ps -> ( ch -> ta ) )
Theorem	eel021old 37122	el021old 37123 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ( ps /\ ch ) -> th )   &    |- ( ( ph /\ th ) -> ta )   =>    |- ( ( ps /\ ch ) -> ta )
Theorem	el021old 37123	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- (. (. ps ,. ch ). ->. th ).   &    |- ( ( ph /\ th ) -> ta )   =>    |- (. (. ps ,. ch ). ->. ta ).
Theorem	eel132 37124	syl2an 484 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.)
|- ( ph -> ps )   &    |- ( ( ch /\ th ) -> ta )   &    |- ( ( ps /\ ta ) -> et )   =>    |- ( ( ph /\ ch /\ th ) -> et )
Theorem	eel2221 37125	Deduction related to syl3an 1318 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ( th /\ ph ) -> ta )   &    |- ( ( ps /\ ch /\ ta ) -> et )   =>    |- ( ( th /\ ph ) -> et )
Theorem	eel000cT 37126	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ps   &    |- ch   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( T. -> th )
Theorem	eel0TT 37127	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( T. -> ps )   &    |- ( T. -> ch )   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- th
Theorem	eelT00 37128	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( T. -> ph )   &    |- ps   &    |- ch   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- th
Theorem	eelTTT 37129	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( T. -> ph )   &    |- ( T. -> ps )   &    |- ( T. -> ch )   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- th
Theorem	eelT11 37130	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( T. -> ph )   &    |- ( ps -> ch )   &    |- ( ps -> th )   &    |- ( ( ph /\ ch /\ th ) -> ta )   =>    |- ( ps -> ta )
Theorem	eel012 37131	mp3an 1373 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)
|- ph   &    |- ( ps -> ch )   &    |- ( th -> ta )   &    |- ( ( ph /\ ch /\ ta ) -> et )   =>    |- ( ( ps /\ th ) -> et )
Theorem	eel0121 37132	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
|- ph   &    |- ( ps -> ch )   &    |- ( ( ps /\ th ) -> ta )   &    |- ( ( ph /\ ch /\ ta ) -> et )   =>    |- ( ( ps /\ th ) -> et )
Theorem	eelT1 37133	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.)
|- ( T. -> ph )   &    |- ( ps -> ch )   &    |- ( ( ph /\ ch ) -> th )   =>    |- ( ps -> th )
Theorem	eelT12 37134	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( T. -> ph )   &    |- ( ps -> ch )   &    |- ( th -> ta )   &    |- ( ( ph /\ ch /\ ta ) -> et )   =>    |- ( ( ps /\ th ) -> et )
Theorem	eelTT1 37135	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( T. -> ph )   &    |- ( T. -> ps )   &    |- ( ch -> th )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ch -> ta )
Theorem	eelT01 37136	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( T. -> ph )   &    |- ps   &    |- ( ch -> th )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ch -> ta )
Theorem	eel0T1 37137	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( T. -> ps )   &    |- ( ch -> th )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ch -> ta )
Theorem	eel12131 37138	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
|- ( ph -> ps )   &    |- ( ( ph /\ ch ) -> th )   &    |- ( ( ph /\ ta ) -> et )   &    |- ( ( ps /\ th /\ et ) -> ze )   =>    |- ( ( ph /\ ch /\ ta ) -> ze )
Theorem	eel2131 37139	syl2an 484 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ th ) -> ta )   &    |- ( ( ch /\ ta ) -> et )   =>    |- ( ( ph /\ ps /\ th ) -> et )
Theorem	eel3132 37140	syl2an 484 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( th /\ ps ) -> ta )   &    |- ( ( ch /\ ta ) -> et )   =>    |- ( ( ph /\ th /\ ps ) -> et )
Theorem	eel0321old 37141	el0321old 37142 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ( ps /\ ch /\ th ) -> ta )   &    |- ( ( ph /\ ta ) -> et )   =>    |- ( ( ps /\ ch /\ th ) -> et )
Theorem	el0321old 37142	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- (. (. ps ,. ch ,. th ). ->. ta ).   &    |- ( ( ph /\ ta ) -> et )   =>    |- (. (. ps ,. ch ,. th ). ->. et ).
Theorem	eel2122old 37143	el2122old 37144 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ps -> th )   &    |- ( ps -> ta )   &    |- ( ( ch /\ th /\ ta ) -> et )   =>    |- ( ( ph /\ ps ) -> et )
Theorem	el2122old 37144	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. (. ph ,. ps ). ->. ch ).   &    |- (. ps ->. th ).   &    |- (. ps ->. ta ).   &    |- ( ( ch /\ th /\ ta ) -> et )   =>    |- (. (. ph ,. ps ). ->. et ).
Theorem	eel0001 37145	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
|- ph   &    |- ps   &    |- ch   &    |- ( th -> ta )   &    |- ( ( ( ( ph /\ ps ) /\ ch ) /\ ta ) -> et )   =>    |- ( th -> et )
Theorem	eel0000 37146	Elimination rule similar to mp4an 684, except with a left-nested conjunction unification theorem. (Contributed by Alan Sare, 17-Oct-2017.)
|- ph   &    |- ps   &    |- ch   &    |- th   &    |- ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) -> ta )   =>    |- ta
Theorem	eel1111 37147	Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1280 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ( ( ( ps /\ ch ) /\ th ) /\ ta ) -> et )   =>    |- ( ph -> et )
Theorem	eel00001 37148	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
|- ph   &    |- ps   &    |- ch   &    |- th   &    |- ( ta -> et )   &    |- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ et ) -> ze )   =>    |- ( ta -> ze )
Theorem	eel00000 37149	Elimination rule similar eel0000 37146, except with five hpothesis steps. (Contributed by Alan Sare, 17-Oct-2017.)
|- ph   &    |- ps   &    |- ch   &    |- th   &    |- ta   &    |- ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) -> et )   =>    |- et
Theorem	eel11111 37150	Five-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc 1288 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> et )   &    |- ( ( ( ( ( ps /\ ch ) /\ th ) /\ ta ) /\ et ) -> ze )   =>    |- ( ph -> ze )
Theorem	e12 37151	A virtual deduction elimination rule (see sylsyld 58). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ph ,. ch ->. th ).   &    |- ( ps -> ( th -> ta ) )   =>    |- (. ph ,. ch ->. ta ).
Theorem	e12an 37152	Conjunction form of e12 37151 (see syl6an 552). (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ph ,. ch ->. th ).   &    |- ( ( ps /\ th ) -> ta )   =>    |- (. ph ,. ch ->. ta ).
Theorem	el12 37153	Virtual deduction form of syl2an 484. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ta ->. ch ).   &    |- ( ( ps /\ ch ) -> th )   =>    |- (. (. ph ,. ta ). ->. th ).
Theorem	e20 37154	A virtual deduction elimination rule (see syl6mpi 64). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- th   &    |- ( ch -> ( th -> ta ) )   =>    |- (. ph ,. ps ->. ta ).
Theorem	e20an 37155	Conjunction form of e20 37154. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- th   &    |- ( ( ch /\ th ) -> ta )   =>    |- (. ph ,. ps ->. ta ).
Theorem	ee20an 37156	e20an 37155 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   &    |- th   &    |- ( ( ch /\ th ) -> ta )   =>    |- ( ph -> ( ps -> ta ) )
Theorem	e21 37157	A virtual deduction elimination rule (see syl6ci 67). (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- (. ph ->. th ).   &    |- ( ch -> ( th -> ta ) )   =>    |- (. ph ,. ps ->. ta ).
Theorem	e21an 37158	Conjunction form of e21 37157. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- (. ph ->. th ).   &    |- ( ( ch /\ th ) -> ta )   =>    |- (. ph ,. ps ->. ta ).
Theorem	ee21an 37159	e21an 37158 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> th )   &    |- ( ( ch /\ th ) -> ta )   =>    |- ( ph -> ( ps -> ta ) )
Theorem	e333 37160	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ch ->. th ).   &    |- (. ph ,. ps ,. ch ->. ta ).   &    |- (. ph ,. ps ,. ch ->. et ).   &    |- ( th -> ( ta -> ( et -> ze ) ) )   =>    |- (. ph ,. ps ,. ch ->. ze ).
Theorem	e33 37161	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ch ->. th ).   &    |- (. ph ,. ps ,. ch ->. ta ).   &    |- ( th -> ( ta -> et ) )   =>    |- (. ph ,. ps ,. ch ->. et ).
Theorem	e33an 37162	Conjunction form of e33 37161. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ch ->. th ).   &    |- (. ph ,. ps ,. ch ->. ta ).   &    |- ( ( th /\ ta ) -> et )   =>    |- (. ph ,. ps ,. ch ->. et ).
Theorem	ee33an 37163	e33an 37162 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   &    |- ( ph -> ( ps -> ( ch -> ta ) ) )   &    |- ( ( th /\ ta ) -> et )   =>    |- ( ph -> ( ps -> ( ch -> et ) ) )
Theorem	e3 37164	Meta-connective form of syl8 72. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ch ->. th ).   &    |- ( th -> ta )   =>    |- (. ph ,. ps ,. ch ->. ta ).
Theorem	e3bi 37165	Biconditional form of e3 37164. syl8ib 239 is e3bi 37165 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ch ->. th ).   &    |- ( th <-> ta )   =>    |- (. ph ,. ps ,. ch ->. ta ).
Theorem	e3bir 37166	Right biconditional form of e3 37164. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ch ->. th ).   &    |- ( ta <-> th )   =>    |- (. ph ,. ps ,. ch ->. ta ).
Theorem	e03 37167	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- (. ps ,. ch ,. th ->. ta ).   &    |- ( ph -> ( ta -> et ) )   =>    |- (. ps ,. ch ,. th ->. et ).
Theorem	ee03 37168	e03 37167 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ps -> ( ch -> ( th -> ta ) ) )   &    |- ( ph -> ( ta -> et ) )   =>    |- ( ps -> ( ch -> ( th -> et ) ) )
Theorem	e03an 37169	Conjunction form of e03 37167. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- (. ps ,. ch ,. th ->. ta ).   &    |- ( ( ph /\ ta ) -> et )   =>    |- (. ps ,. ch ,. th ->. et ).
Theorem	ee03an 37170	Conjunction form of ee03 37168. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ps -> ( ch -> ( th -> ta ) ) )   &    |- ( ( ph /\ ta ) -> et )   =>    |- ( ps -> ( ch -> ( th -> et ) ) )
Theorem	e30 37171	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ch ->. th ).   &    |- ta   &    |- ( th -> ( ta -> et ) )   =>    |- (. ph ,. ps ,. ch ->. et ).
Theorem	ee30 37172	e30 37171 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   &    |- ta   &    |- ( th -> ( ta -> et ) )   =>    |- ( ph -> ( ps -> ( ch -> et ) ) )
Theorem	e30an 37173	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   &    |- ( ( th /\ ta ) -> et )   =>    |- (. ph ,. ps ,. ch ->. et ).
Theorem	ee30an 37174	Conjunction form of ee30 37172. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   &    |- ta   &    |- ( ( th /\ ta ) -> et )   =>    |- ( ph -> ( ps -> ( ch -> et ) ) )
Theorem	e13 37175	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ph ,. ch ,. th ->. ta ).   &    |- ( ps -> ( ta -> et ) )   =>    |- (. ph ,. ch ,. th ->. et ).
Theorem	e13an 37176	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 ->. ta ).   &    |- ( ( ps /\ ta ) -> et )   =>    |- (. ph ,. ch ,. th ->. et ).
Theorem	ee13an 37177	e13an 37176 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ps )   &    |- ( ph -> ( ch -> ( th -> ta ) ) )   &    |- ( ( ps /\ ta ) -> et )   =>    |- ( ph -> ( ch -> ( th -> et ) ) )
Theorem	e31 37178	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ch ->. th ).   &    |- (. ph ->. ta ).   &    |- ( th -> ( ta -> et ) )   =>    |- (. ph ,. ps ,. ch ->. et ).
Theorem	ee31 37179	e31 37178 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   &    |- ( ph -> ta )   &    |- ( th -> ( ta -> et ) )   =>    |- ( ph -> ( ps -> ( ch -> et ) ) )
Theorem	e31an 37180	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 ).   &    |- ( ( th /\ ta ) -> et )   =>    |- (. ph ,. ps ,. ch ->. et ).
Theorem	ee31an 37181	e31an 37180 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   &    |- ( ph -> ta )   &    |- ( ( th /\ ta ) -> et )   =>    |- ( ph -> ( ps -> ( ch -> et ) ) )
Theorem	e23 37182	A virtual deduction elimination rule (see syl10 75). (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- (. ph ,. ps ,. th ->. ta ).   &    |- ( ch -> ( ta -> et ) )   =>    |- (. ph ,. ps ,. th ->. et ).
Theorem	e23an 37183	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 /\ ta ) -> et )   =>    |- (. ph ,. ps ,. th ->. et ).
Theorem	ee23an 37184	e23an 37183 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( ps -> ( th -> ta ) ) )   &    |- ( ( ch /\ ta ) -> et )   =>    |- ( ph -> ( ps -> ( th -> et ) ) )
Theorem	e32 37185	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ch ->. th ).   &    |- (. ph ,. ps ->. ta ).   &    |- ( th -> ( ta -> et ) )   =>    |- (. ph ,. ps ,. ch ->. et ).
Theorem	ee32 37186	e32 37185 without virtual deductions. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   &    |- ( ph -> ( ps -> ta ) )   &    |- ( th -> ( ta -> et ) )   =>    |- ( ph -> ( ps -> ( ch -> et ) ) )
Theorem	e32an 37187	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 ).   &    |- ( ( th /\ ta ) -> et )   =>    |- (. ph ,. ps ,. ch ->. et ).
Theorem	ee32an 37188	e33an 37162 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ( ch -> th ) ) )   &    |- ( ph -> ( ps -> ta ) )   &    |- ( ( th /\ ta ) -> et )   =>    |- ( ph -> ( ps -> ( ch -> et ) ) )
Theorem	e123 37189	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ph ,. ch ->. th ).   &    |- (. ph ,. ch ,. ta ->. et ).   &    |- ( ps -> ( th -> ( et -> ze ) ) )   =>    |- (. ph ,. ch ,. ta ->. ze ).
Theorem	ee123 37190	e123 37189 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ps )   &    |- ( ph -> ( ch -> th ) )   &    |- ( ph -> ( ch -> ( ta -> et ) ) )   &    |- ( ps -> ( th -> ( et -> ze ) ) )   =>    |- ( ph -> ( ch -> ( ta -> ze ) ) )
Theorem	el123 37191	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ->. ps ).   &    |- (. ch ->. th ).   &    |- (. ta ->. et ).   &    |- ( ( ps /\ th /\ et ) -> ze )   =>    |- (. (. ph ,. ch ,. ta ). ->. ze ).
Theorem	e233 37192	A virtual deduction elimination rule. (Contributed by Alan Sare, 29-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ->. ch ).   &    |- (. ph ,. ps ,. th ->. ta ).   &    |- (. ph ,. ps ,. th ->. et ).   &    |- ( ch -> ( ta -> ( et -> ze ) ) )   =>    |- (. ph ,. ps ,. th ->. ze ).
Theorem	e323 37193	A virtual deduction elimination rule. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. ph ,. ps ,. ch ->. th ).   &    |- (. ph ,. ps ->. ta ).   &    |- (. ph ,. ps ,. ch ->. et ).   &    |- ( th -> ( ta -> ( et -> ze ) ) )   =>    |- (. ph ,. ps ,. ch ->. ze ).
Theorem	e000 37194	A virtual deduction elimination rule. The non-virtual deduction form of e000 37194 is the virtual deduction form. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ps   &    |- ch   &    |- ( ph -> ( ps -> ( ch -> th ) ) )   =>    |- th
Theorem	e00 37195	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.)
|- ph   &    |- ps   &    |- ( ph -> ( ps -> ch ) )   =>    |- ch
Theorem	e00an 37196	Elimination rule identical to mp2an 683. The non-virtual deduction form is the virtual deduction form, which is mp2an 683. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ps   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ch
Theorem	eel00cT 37197	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ps   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ( T. -> ch )
Theorem	eelTT 37198	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( T. -> ph )   &    |- ( T. -> ps )   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ch
Theorem	e0a 37199	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.)
|- ph   &    |- ( ph -> ps )   =>    |- ps
Theorem	eelT 37200	An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( T. -> ph )   &    |- ( ph -> ps )   =>    |- ps