P. 334 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33301-33400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	e200 33301	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 33302	e200 33301 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 33303	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 33304	e221 33303 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 33305	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 33306	e212 33305 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 33307	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 33308	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 33309	e112 33308 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 33310	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 33311	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 33312	e211 33311 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 33313	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 33314	e210 33313 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 33315	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 33316	e201 33315 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 33317	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 33318	Virtual deduction rule e120 33317 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 33319	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 33320	e021 33319 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 33321	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 33322	e012 33321 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 33323	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 33324	e102 33323 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 33325	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 33326	Conjunction form of e22 33325. (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 33327	e22an 33326 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 33328	A virtual deduction elimination rule (see syl3c 61). (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 33329	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 33330	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 33331	e110 33330 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 33332	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 ).
Theorem	ee101 33333	e101 33332 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 33334	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 33335	e011 33334 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 33336	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 33337	e100 33336 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 33338	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 33339	e010 33338 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 33340	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 33341	e001 33340 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 33342	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 33343	Conjunction form of e11 33342. (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 33344	e11an 33343 without virtual deductions. syl22anc 1230 is also e11an 33343 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 33345	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 33346	Conjunction form of e01 33345. (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 33347	e01an 33346 without virtual deductions. sylancr 663 is also a form of e01an 33346 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 33348	A virtual deduction elimination rule (see mpisyl 18). (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 33349	Conjunction form of e10 33348. (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 33350	e10an 33349 without virtual deductions. sylancl 662 is also e10an 33349 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 33351	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 33352	Conjunction form of e02 33351. (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 33353	e02an 33352 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 33354	el021old 33355 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 33355	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 33356	syl2an 477 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 33357	Deduction related to syl3an 1271 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	eel112 33358	syl3an 1271 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( th -> ta )   &    |- ( ( ps /\ ch /\ ta ) -> et )   =>    |- ( ( ph /\ th ) -> et )
Theorem	eel000cT 33359	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 33360	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 33361	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 33362	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	eel011 33363	mp3an 1325 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)
|- ph   &    |- ( ps -> ch )   &    |- ( ps -> th )   &    |- ( ( ph /\ ch /\ th ) -> ta )   =>    |- ( ps -> ta )
Theorem	eelT11 33364	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 33365	mp3an 1325 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 33366	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 33367	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 33368	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	eel001 33369	mp3an 1325 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)
|- ph   &    |- ps   &    |- ( ch -> th )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ch -> ta )
Theorem	eelTT1 33370	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 33371	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 33372	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	eel121 33373	syl2an 477 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
|- ( ph -> ps )   &    |- ( ( ph /\ ch ) -> th )   &    |- ( ( ps /\ th ) -> ta )   =>    |- ( ( ph /\ ch ) -> ta )
Theorem	eel12131 33374	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 33375	syl2an 477 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 33376	syl2an 477 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	eel32131 33377	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
|- ( ( ph /\ ps /\ ch ) -> th )   &    |- ( ( ph /\ ch ) -> ta )   &    |- ( ( th /\ ta ) -> et )   =>    |- ( ( ph /\ ps /\ ch ) -> et )
Theorem	eel221 33378	syl2an 477 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
|- ( ph -> ps )   &    |- ( ( ch /\ ph ) -> th )   &    |- ( ( ps /\ th ) -> ta )   =>    |- ( ( ch /\ ph ) -> ta )
Theorem	eel0321old 33379	el0321old 33380 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 33380	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 33381	el2122old 33382 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 33382	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 33383	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
|- ph   &    |- ps   &    |- ch   &    |- ( th -> ta )   &    |- ( ( ( ( ph /\ ps ) /\ ch ) /\ ta ) -> et )   =>    |- ( th -> et )
Theorem	eel0000 33384	Elimination rule similar to mp4an 673, 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 33385	4 hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1233 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 33386	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 33387	Elimination rule similar eel0000 33384, 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 33388	5 hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc 1241 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 33389	A virtual deduction elimination rule (see sylsyld 56). (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 33390	Conjunction form of e12 33389 (see syl6an 545). (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 33391	Virtual deduction form of syl2an 477. (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 33392	A virtual deduction elimination rule (see syl6mpi 62). (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 33393	Conjunction form of e20 33392. (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 33394	e20an 33393 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 33395	A virtual deduction elimination rule (see syl6ci 65). (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 33396	Conjunction form of e21 33395. (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 33397	e21an 33396 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 33398	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 33399	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 33400	Conjunction form of e33 33399. (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 ).