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
Theorem	e020 37001	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 37002	e020 37001 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 37003	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 37004	e200 37003 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 37005	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 37006	e221 37005 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 37007	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 37008	e212 37007 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 37009	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 37010	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 37011	e112 37010 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 37012	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 37013	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 37014	e211 37013 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 37015	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 37016	e210 37015 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 37017	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 37018	e201 37017 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 37019	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 37020	Virtual deduction rule e120 37019 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 37021	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 37022	e021 37021 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 37023	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 37024	e012 37023 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 37025	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 37026	e102 37025 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 37027	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 37028	Conjunction form of e22 37027. (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 37029	e22an 37028 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 37030	A virtual deduction elimination rule (see syl3c 64). (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 37031	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 37032	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 37033	e110 37032 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 37034	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 37035	e101 37034 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 37036	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 37037	e011 37036 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 37038	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 37039	e100 37038 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 37040	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 37041	e010 37040 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 37042	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 37043	e001 37042 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 37044	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 37045	Conjunction form of e11 37044. (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 37046	e11an 37045 without virtual deductions. syl22anc 1266 is also e11an 37045 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 37047	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 37048	Conjunction form of e01 37047. (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 37049	e01an 37048 without virtual deductions. sylancr 668 is also a form of e01an 37048 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 37050	A virtual deduction elimination rule (see mpisyl 22). (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 37051	Conjunction form of e10 37050. (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 37052	e10an 37051 without virtual deductions. sylancl 667 is also e10an 37051 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 37053	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 37054	Conjunction form of e02 37053. (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 37055	e02an 37054 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 37056	el021old 37057 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 37057	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 37058	syl2an 480 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 37059	Deduction related to syl3an 1307 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 37060	syl3an 1307 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 37061	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 37062	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 37063	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 37064	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 37065	mp3an 1361 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 37066	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 37067	mp3an 1361 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 37068	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 37069	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 37070	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 37071	mp3an 1361 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 37072	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 37073	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 37074	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 37075	syl2an 480 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 37076	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 37077	syl2an 480 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 37078	syl2an 480 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 37079	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	eel0321old 37080	el0321old 37081 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 37081	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 37082	el2122old 37083 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 37083	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 37084	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
|- ph   &    |- ps   &    |- ch   &    |- ( th -> ta )   &    |- ( ( ( ( ph /\ ps ) /\ ch ) /\ ta ) -> et )   =>    |- ( th -> et )
Theorem	eel0000 37085	Elimination rule similar to mp4an 678, 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 37086	Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1269 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 37087	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 37088	Elimination rule similar eel0000 37085, 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 37089	Five-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc 1277 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 37090	A virtual deduction elimination rule (see sylsyld 59). (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 37091	Conjunction form of e12 37090 (see syl6an 548). (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 37092	Virtual deduction form of syl2an 480. (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 37093	A virtual deduction elimination rule (see syl6mpi 65). (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 37094	Conjunction form of e20 37093. (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 37095	e20an 37094 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 37096	A virtual deduction elimination rule (see syl6ci 68). (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 37097	Conjunction form of e21 37096. (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 37098	e21an 37097 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 37099	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 37100	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 ).