P. 447 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44601-44700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	in3 44601	The virtual deduction introduction rule of converting the end virtual hypothesis of 3 virtual hypotheses into an antecedent. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   (𝜒 → 𝜃)   )
Theorem	iin3 44602	in3 44601 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
Theorem	in3an 44603	The virtual deduction introduction rule converting the second conjunct of the third virtual hypothesis into the antecedent of the conclusion. exp4a 431 is the non-virtual deduction form of in3an 44603. (Contributed by Alan Sare, 25-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   (𝜒 ∧ 𝜃)   ▶   𝜏   )    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   (𝜃 → 𝜏)   )
Theorem	int3 44604	The virtual deduction introduction rule of converting the end virtual hypothesis of 3 virtual hypotheses into an antecedent. Conventional form of int3 44604 is 3expia 1121. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   (   𝜑   ,   𝜓   ,   𝜒   )   ▶   𝜃   )    ⇒   ⊢ (   (   𝜑   ,   𝜓   )   ▶   (𝜒 → 𝜃)   )
Theorem	idn2 44605	Virtual deduction identity rule which is idd 24 with virtual deduction symbols. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜓   )
Theorem	iden2 44606	Virtual deduction identity rule. simpr 484 in conjunction form Virtual Deduction notation. (Contributed by Alan Sare, 5-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   (   𝜑   ,   𝜓   )   ▶   𝜓   )
Theorem	idn3 44607	Virtual deduction identity rule for three virtual hypotheses. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜒   )
Theorem	gen11 44608*	Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis. alrimiv 1926 is gen11 44608 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ▶   ∀𝑥𝜓   )
Theorem	gen11nv 44609	Virtual deduction generalizing rule for one quantifying variable and one virtual hypothesis without distinct variables. alrimih 1823 is gen11nv 44609 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (   𝜑   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ▶   ∀𝑥𝜓   )
Theorem	gen12 44610*	Virtual deduction generalizing rule for two quantifying variables and one virtual hypothesis. gen12 44610 is alrimivv 1927 with virtual deductions. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ▶   ∀𝑥∀𝑦𝜓   )
Theorem	gen21 44611*	Virtual deduction generalizing rule for one quantifying variables and two virtual hypothesis. gen21 44611 is alrimdv 1928 with virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   ∀𝑥𝜒   )
Theorem	gen21nv 44612	Virtual deduction form of alrimdh 1862. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   ∀𝑥𝜒   )
Theorem	gen31 44613*	Virtual deduction generalizing rule for one quantifying variable and three virtual hypothesis. gen31 44613 is ggen31 44537 with virtual deductions. (Contributed by Alan Sare, 22-Jun-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   ∀𝑥𝜃   )
Theorem	gen22 44614*	Virtual deduction generalizing rule for two quantifying variables and two virtual hypothesis. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   ∀𝑥∀𝑦𝜒   )
Theorem	ggen22 44615*	gen22 44614 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → ∀𝑥∀𝑦𝜒))
Theorem	exinst 44616	Existential Instantiation. Virtual deduction form of exlimexi 44516. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (   ∃𝑥𝜑   ,   𝜑   ▶   𝜓   )    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	exinst01 44617	Existential Instantiation. Virtual Deduction rule corresponding to a special case of the Natural Deduction Sequent Calculus rule called Rule C in [Margaris] p. 79 and E ∃ in Table 1 on page 4 of the paper "Extracting information from intermediate T-systems" (2000) presented at IMLA99 by Mauro Ferrari, Camillo Fiorentini, and Pierangelo Miglioli. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ∃𝑥𝜓    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	exinst11 44618	Existential Instantiation. Virtual Deduction rule corresponding to a special case of the Natural Deduction Sequent Calculus rule called Rule C in [Margaris] p. 79 and E ∃ in Table 1 on page 4 of the paper "Extracting information from intermediate T-systems" (2000) presented at IMLA99 by Mauro Ferrari, Camillo Fiorentini, and Pierangelo Miglioli. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   ∃𝑥𝜓   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	e1a 44619	A Virtual deduction elimination rule. syl 17 is e1a 44619 without virtual deductions. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	el1 44620	A Virtual deduction elimination rule. syl 17 is el1 44620 without virtual deductions. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	e1bi 44621	Biconditional form of e1a 44619. sylib 218 is e1bi 44621 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	e1bir 44622	Right biconditional form of e1a 44619. sylibr 234 is e1bir 44622 without virtual deductions. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (𝜒 ↔ 𝜓)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	e2 44623	A virtual deduction elimination rule. syl6 35 is e2 44623 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
Theorem	e2bi 44624	Biconditional form of e2 44623. imbitrdi 251 is e2bi 44624 without virtual deductions. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
Theorem	e2bir 44625	Right biconditional form of e2 44623. imbitrrdi 252 is e2bir 44625 without virtual deductions. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (𝜃 ↔ 𝜒)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
Theorem	ee223 44626	e223 44627 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    &   ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜁)))
Theorem	e223 44627	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜏   ▶   𝜂   )    &   ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜏   ▶   𝜁   )
Theorem	e222 44628	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	e220 44629	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee220 44630	e220 44629 without virtual deductions. (Contributed by Alan Sare, 12-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e202 44631	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee202 44632	e202 44631 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜃    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e022 44633	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee022 44634	e022 44633 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ (𝜓 → (𝜒 → 𝜏))    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜒 → 𝜂))
Theorem	e002 44635	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	ee002 44636	e002 44635 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (𝜒 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜒 → (𝜃 → 𝜂))
Theorem	e020 44637	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee020 44638	e020 44637 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ 𝜏    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜒 → 𝜂))
Theorem	e200 44639	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee200 44640	e200 44639 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜃    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e221 44641	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee221 44642	e221 44641 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e212 44643	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee212 44644	e212 44643 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e122 44645	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜂   )
Theorem	e112 44646	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜃   ▶   𝜂   )
Theorem	ee112 44647	e112 44646 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜃 → 𝜂))
Theorem	e121 44648	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜂   )
Theorem	e211 44649	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee211 44650	e211 44649 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e210 44651	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee210 44652	e210 44651 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e201 44653	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee201 44654	e201 44653 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜃    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e120 44655	A virtual deduction elimination rule. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜂   )
Theorem	ee120 44656	Virtual deduction rule e120 44655 without virtual deduction symbols. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ 𝜏    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜂))
Theorem	e021 44657	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜓   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee021 44658	e021 44657 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ (𝜓 → 𝜏)    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜒 → 𝜂))
Theorem	e012 44659	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜃   ▶   𝜂   )
Theorem	ee012 44660	e012 44659 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜃 → 𝜂))
Theorem	e102 44661	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ (   𝜑   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜃   ▶   𝜂   )
Theorem	ee102 44662	e102 44661 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜃 → 𝜂))
Theorem	e22 44663	A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ (𝜒 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	e22an 44664	Conjunction form of e22 44663. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	ee22an 44665	e22an 44664 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜏))
Theorem	e111 44666	A virtual deduction elimination rule (see syl3c 66). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	e1111 44667	A virtual deduction elimination rule. (Contributed by Alan Sare, 6-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))    ⇒   ⊢ (   𝜑   ▶   𝜂   )
Theorem	e110 44668	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee110 44669	e110 44668 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e101 44670	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee101 44671	e101 44670 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e011 44672	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (   𝜓   ▶   𝜃   )    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜓   ▶   𝜏   )
Theorem	ee011 44673	e011 44672 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	e100 44674	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee100 44675	e100 44674 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e010 44676	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜓   ▶   𝜏   )
Theorem	ee010 44677	e010 44676 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ 𝜃    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	e001 44678	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (   𝜒   ▶   𝜃   )    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜒   ▶   𝜏   )
Theorem	ee001 44679	e001 44678 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	e11 44680	A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ (𝜓 → (𝜒 → 𝜃))    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	e11an 44681	Conjunction form of e11 44680. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	ee11an 44682	e11an 44681 without virtual deductions. syl22anc 838 is also e11an 44681 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.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	e01 44683	A virtual deduction elimination rule. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (𝜑 → (𝜒 → 𝜃))    ⇒   ⊢ (   𝜓   ▶   𝜃   )
Theorem	e01an 44684	Conjunction form of e01 44683. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   𝜓   ▶   𝜃   )
Theorem	ee01an 44685	e01an 44684 without virtual deductions. sylancr 587 is also a form of e01an 44684 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.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	e10 44686	A virtual deduction elimination rule (see mpisyl 21). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ (𝜓 → (𝜒 → 𝜃))    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	e10an 44687	Conjunction form of e10 44686. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	ee10an 44688	e10an 44687 without virtual deductions. sylancl 586 is also e10an 44687 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.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	e02 44689	A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜑 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	e02an 44690	Conjunction form of e02 44689. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	ee02an 44691	e02an 44690 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜓 → (𝜒 → 𝜏))
Theorem	eel021old 44692	el021old 44693 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜏)
Theorem	el021old 44693	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   (   𝜓   ,   𝜒   )   ▶   𝜃   )    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   (   𝜓   ,   𝜒   )   ▶   𝜏   )
Theorem	eel132 44694	syl2an 596 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂)
Theorem	eel000cT 44695	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (⊤ → 𝜃)
Theorem	eel0TT 44696	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (⊤ → 𝜓)    &   ⊢ (⊤ → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	eelT00 44697	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	eelTTT 44698	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (⊤ → 𝜓)    &   ⊢ (⊤ → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	eelT11 44699	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	eelT1 44700	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.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)