P. 333 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33201-33300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eelT00 33201	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 33202	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 33203	mp3an 1323 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 33204	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 33205	mp3an 1323 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 33206	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 33207	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 33208	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 33209	mp3an 1323 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 33210	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 33211	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 33212	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 33213	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 33214	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 33215	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 33216	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 33217	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 33218	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 33219	el0321old 33220 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 33220	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 33221	el2122old 33222 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 33222	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 33223	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
|- ph   &    |- ps   &    |- ch   &    |- ( th -> ta )   &    |- ( ( ( ( ph /\ ps ) /\ ch ) /\ ta ) -> et )   =>    |- ( th -> et )
Theorem	eel0000 33224	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 33225	4 hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1231 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 33226	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 33227	Elimination rule similar eel0000 33224, 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 33228	5 hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc 1239 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 33229	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 33230	Conjunction form of e12 33229 (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 33231	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 33232	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 33233	Conjunction form of e20 33232. (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 33234	e20an 33233 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 33235	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 33236	Conjunction form of e21 33235. (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 33237	e21an 33236 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 33238	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 33239	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 33240	Conjunction form of e33 33239. (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 33241	e33an 33240 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 33242	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 33243	Biconditional form of e3 33242. syl8ib 231 is e3bi 33243 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 33244	Right biconditional form of e3 33242. (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 33245	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 33246	e03 33245 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 33247	Conjunction form of e03 33245. (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 33248	Conjunction form of ee03 33246. (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 33249	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 33250	e30 33249 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 33251	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 33252	Conjunction form of ee30 33250. (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 33253	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 33254	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 33255	e13an 33254 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 33256	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 33257	e31 33256 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 33258	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 33259	e31an 33258 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 33260	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 33261	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 33262	e23an 33261 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 33263	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 33264	e32 33263 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 33265	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 33266	e33an 33240 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 33267	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 33268	e123 33267 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 33269	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 33270	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 33271	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 33272	A virtual deduction elimination rule. The non-virtual deduction form of e000 33272 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 33273	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 33274	Elimination rule identical to mp2an 672. The non-virtual deduction form is the virtual deduction form, which is mp2an 672. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ph   &    |- ps   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ch
Theorem	eel00cT 33275	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 33276	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 33277	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 33278	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 33279	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 33280	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 33281	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 33282	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 33283	Convention notation form of un0.1 33284. (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 33284	T. is the constant true, a tautology (see df-tru 1384). 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 33285	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 1384. (Revised by David A. Wheeler, 8-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( T. /\ ph ) -> ps )   =>    |- ( ph -> ps )
Theorem	uunT1p1 33286	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 33287	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 33288	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 33289	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 33290	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 33291	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 33292	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 33293	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 33294	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 33295	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 )
Theorem	uun2131 33296	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 ) ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	uun2131p1 33297	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 /\ ch ) /\ ( ph /\ ps ) ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	uunTT1 33298	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.)
|- ( ( T. /\ T. /\ ph ) -> ps )   =>    |- ( ph -> ps )
Theorem	uunTT1p1 33299	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.)
|- ( ( T. /\ ph /\ T. ) -> ps )   =>    |- ( ph -> ps )
Theorem	uunTT1p2 33300	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. /\ T. ) -> ps )   =>    |- ( ph -> ps )