P. 340 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33901-34000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eel132 33901	syl2an 475 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 33902	Deduction related to syl3an 1268 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 33903	syl3an 1268 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 33904	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 33905	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 33906	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 33907	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 33908	mp3an 1322 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 33909	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 33910	mp3an 1322 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 33911	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 33912	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 33913	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 33914	mp3an 1322 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 33915	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 33916	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 33917	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 33918	syl2an 475 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 33919	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 33920	syl2an 475 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 33921	syl2an 475 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 33922	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 33923	syl2an 475 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 33924	el0321old 33925 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 33925	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 33926	el2122old 33927 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 33927	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 33928	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
|- ph   &    |- ps   &    |- ch   &    |- ( th -> ta )   &    |- ( ( ( ( ph /\ ps ) /\ ch ) /\ ta ) -> et )   =>    |- ( th -> et )
Theorem	eel0000 33929	Elimination rule similar to mp4an 671, 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 33930	4 hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1230 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 33931	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 33932	Elimination rule similar eel0000 33929, 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 33933	5 hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc 1238 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 33934	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 33935	Conjunction form of e12 33934 (see syl6an 543). (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 33936	Virtual deduction form of syl2an 475. (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 33937	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 33938	Conjunction form of e20 33937. (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 33939	e20an 33938 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 33940	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 33941	Conjunction form of e21 33940. (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 33942	e21an 33941 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 33943	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 33944	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 33945	Conjunction form of e33 33944. (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 33946	e33an 33945 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 33947	Meta-connective form of syl8 70. (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 33948	Biconditional form of e3 33947. syl8ib 231 is e3bi 33948 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 33949	Right biconditional form of e3 33947. (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 33950	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 33951	e03 33950 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 33952	Conjunction form of e03 33950. (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 33953	Conjunction form of ee03 33951. (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 33954	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 33955	e30 33954 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 33956	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 33957	Conjunction form of ee30 33955. (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 33958	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 33959	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 33960	e13an 33959 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 33961	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 33962	e31 33961 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 33963	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 33964	e31an 33963 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 33965	A virtual deduction elimination rule (see syl10 73). (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 33966	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 33967	e23an 33966 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 33968	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 33969	e32 33968 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 33970	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 33971	e33an 33945 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 33972	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 33973	e123 33972 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 33974	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 33975	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 33976	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 33977	A virtual deduction elimination rule. The non-virtual deduction form of e000 33977 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 33978	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 33979	Elimination rule identical to mp2an 670. The non-virtual deduction form is the virtual deduction form, which is mp2an 670. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ps   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ch
Theorem	eel00cT 33980	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 33981	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 33982	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 33983	An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( T. -> ph )   &    |- ( ph -> ps )   =>    |- ps
Theorem	eel0cT 33984	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ph -> ps )   =>    |- ( T. -> ps )
Theorem	eelT0 33985	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( T. -> ph )   &    |- ps   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ch
Theorem	e0bi 33986	Elimination rule identical to mpbi 208. The non-virtual deduction form is the virtual deduction form, which is mpbi 208. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ph <-> ps )   =>    |- ps
Theorem	e0bir 33987	Elimination rule identical to mpbir 209. The non-virtual deduction form is the virtual deduction form, which is mpbir 209. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ( ps <-> ph )   =>    |- ps
Theorem	uun0.1 33988	Convention notation form of un0.1 33989. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( T. -> ph )   &    |- ( ps -> ch )   &    |- ( ( T. /\ ps ) -> th )   =>    |- ( ps -> th )
Theorem	un0.1 33989	T. is the constant true, a tautology (see df-tru 1401). Kleene's "empty conjunction" is logically equivalent to T.. In a virtual deduction we shall interpret T. to be the empty wff or the empty collection of virtual hypotheses. T. in a virtual deduction translated into conventional notation we shall interpret to be Kleene's empty conjunction. If th is true given the empty collection of virtual hypotheses and another collection of virtual hypotheses, then it is true given only the other collection of virtual hypotheses. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. T. ->. ph ).   &    |- (. ps ->. ch ).   &    |- (. (. T. ,. ps ). ->. th ).   =>    |- (. ps ->. th ).
Theorem	uunT1 33990	A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) Proof was revised to accomodate a possible future version of df-tru 1401. (Revised by David A. Wheeler, 8-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( T. /\ ph ) -> ps )   =>    |- ( ph -> ps )
Theorem	uunT1p1 33991	A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ph /\ T. ) -> ps )   =>    |- ( ph -> ps )
Theorem	uunT21 33992	A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( T. /\ ( ph /\ ps ) ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	uun121 33993	A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ph /\ ( ph /\ ps ) ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	uun121p1 33994	A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ( ph /\ ps ) /\ ph ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	uun132 33995	A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ph /\ ( ps /\ ch ) ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	uun132p1 33996	A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ( ps /\ ch ) /\ ph ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	anabss7p1 33997	A deduction unionizing a non-unionized collection of virtual hypotheses. This would have been named uun221 if the 0th permutation did not exist in set.mm as anabss7 819. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ( ps /\ ph ) /\ ph ) -> ch )   =>    |- ( ( ps /\ ph ) -> ch )
Theorem	un10 33998	A unionizing deduction (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. (. ph ,. T. ). ->. ps ).   =>    |- (. ph ->. ps ).
Theorem	un01 33999	A unionizing deduction (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (. (. T. ,. ph ). ->. ps ).   =>    |- (. ph ->. ps ).
Theorem	un2122 34000	A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ( ph /\ ps ) /\ ps /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )