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	el1 44601	A Virtual deduction elimination rule. syl 17 is el1 44601 without virtual deductions. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	e1bi 44602	Biconditional form of e1a 44600. sylib 218 is e1bi 44602 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	e1bir 44603	Right biconditional form of e1a 44600. sylibr 234 is e1bir 44603 without virtual deductions. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (𝜒 ↔ 𝜓)    ⇒   ⊢ (   𝜑   ▶   𝜒   )
Theorem	e2 44604	A virtual deduction elimination rule. syl6 35 is e2 44604 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
Theorem	e2bi 44605	Biconditional form of e2 44604. imbitrdi 251 is e2bi 44605 without virtual deductions. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
Theorem	e2bir 44606	Right biconditional form of e2 44604. imbitrrdi 252 is e2bir 44606 without virtual deductions. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (𝜃 ↔ 𝜒)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )
Theorem	ee223 44607	e223 44608 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    &   ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜁)))
Theorem	e223 44608	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜏   ▶   𝜂   )    &   ⊢ (𝜒 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜏   ▶   𝜁   )
Theorem	e222 44609	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	e220 44610	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee220 44611	e220 44610 without virtual deductions. (Contributed by Alan Sare, 12-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e202 44612	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee202 44613	e202 44612 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜃    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e022 44614	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee022 44615	e022 44614 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ (𝜓 → (𝜒 → 𝜏))    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜒 → 𝜂))
Theorem	e002 44616	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	ee002 44617	e002 44616 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (𝜒 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜒 → (𝜃 → 𝜂))
Theorem	e020 44618	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee020 44619	e020 44618 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ 𝜏    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜒 → 𝜂))
Theorem	e200 44620	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee200 44621	e200 44620 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜃    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e221 44622	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee221 44623	e221 44622 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e212 44624	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee212 44625	e212 44624 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e122 44626	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜂   )
Theorem	e112 44627	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜃   ▶   𝜂   )
Theorem	ee112 44628	e112 44627 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜃 → 𝜂))
Theorem	e121 44629	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜂   )
Theorem	e211 44630	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee211 44631	e211 44630 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e210 44632	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee210 44633	e210 44632 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ 𝜏    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e201 44634	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜂   )
Theorem	ee201 44635	e201 44634 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜃    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e120 44636	A virtual deduction elimination rule. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜂   )
Theorem	ee120 44637	Virtual deduction rule e120 44636 without virtual deduction symbols. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ 𝜏    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜂))
Theorem	e021 44638	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜓   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee021 44639	e021 44638 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ (𝜓 → 𝜏)    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜒 → 𝜂))
Theorem	e012 44640	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜃   ▶   𝜂   )
Theorem	ee012 44641	e012 44640 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜃 → 𝜂))
Theorem	e102 44642	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ (   𝜑   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜃   ▶   𝜂   )
Theorem	ee102 44643	e102 44642 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜃 → 𝜂))
Theorem	e22 44644	A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ (𝜒 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	e22an 44645	Conjunction form of e22 44644. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	ee22an 44646	e22an 44645 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜏))
Theorem	e111 44647	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 44648	A virtual deduction elimination rule. (Contributed by Alan Sare, 6-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))    ⇒   ⊢ (   𝜑   ▶   𝜂   )
Theorem	e110 44649	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee110 44650	e110 44649 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e101 44651	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee101 44652	e101 44651 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e011 44653	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (   𝜓   ▶   𝜃   )    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜓   ▶   𝜏   )
Theorem	ee011 44654	e011 44653 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	e100 44655	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee100 44656	e100 44655 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e010 44657	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜓   ▶   𝜏   )
Theorem	ee010 44658	e010 44657 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ 𝜃    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	e001 44659	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (   𝜒   ▶   𝜃   )    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜒   ▶   𝜏   )
Theorem	ee001 44660	e001 44659 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	e11 44661	A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ (𝜓 → (𝜒 → 𝜃))    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	e11an 44662	Conjunction form of e11 44661. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	ee11an 44663	e11an 44662 without virtual deductions. syl22anc 838 is also e11an 44662 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 44664	A virtual deduction elimination rule. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (𝜑 → (𝜒 → 𝜃))    ⇒   ⊢ (   𝜓   ▶   𝜃   )
Theorem	e01an 44665	Conjunction form of e01 44664. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   𝜓   ▶   𝜃   )
Theorem	ee01an 44666	e01an 44665 without virtual deductions. sylancr 587 is also a form of e01an 44665 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 44667	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 44668	Conjunction form of e10 44667. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	ee10an 44669	e10an 44668 without virtual deductions. sylancl 586 is also e10an 44668 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 44670	A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜑 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	e02an 44671	Conjunction form of e02 44670. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	ee02an 44672	e02an 44671 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜓 → (𝜒 → 𝜏))
Theorem	eel021old 44673	el021old 44674 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜏)
Theorem	el021old 44674	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   (   𝜓   ,   𝜒   )   ▶   𝜃   )    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   (   𝜓   ,   𝜒   )   ▶   𝜏   )
Theorem	eel000cT 44675	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (⊤ → 𝜃)
Theorem	eel0TT 44676	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (⊤ → 𝜓)    &   ⊢ (⊤ → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	eelT00 44677	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	eelTTT 44678	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (⊤ → 𝜓)    &   ⊢ (⊤ → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	eelT11 44679	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	eelT1 44680	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.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)
Theorem	eelT12 44681	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜃 → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜓 ∧ 𝜃) → 𝜂)
Theorem	eelTT1 44682	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (⊤ → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	eelT01 44683	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	eel0T1 44684	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (⊤ → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	eel12131 44685	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	eel2131 44686	syl2an 596 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜂)
Theorem	eel3132 44687	syl2an 596 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜂)
Theorem	eel0321old 44688	el0321old 44689 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜂)
Theorem	el0321old 44689	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   (   𝜓   ,   𝜒   ,   𝜃   )   ▶   𝜏   )    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   (   𝜓   ,   𝜒   ,   𝜃   )   ▶   𝜂   )
Theorem	eel2122old 44690	el2122old 44691 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ (𝜓 → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜂)
Theorem	el2122old 44691	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   (   𝜑   ,   𝜓   )   ▶   𝜒   )    &   ⊢ (   𝜓   ▶   𝜃   )    &   ⊢ (   𝜓   ▶   𝜏   )    &   ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   (   𝜑   ,   𝜓   )   ▶   𝜂   )
Theorem	eel0000 44692	Elimination rule similar to mp4an 693, except with a left-nested conjunction unification theorem. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ 𝜏
Theorem	eel00001 44693	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜏 → 𝜂)    &   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜏 → 𝜁)
Theorem	eel00000 44694	Elimination rule similar eel0000 44692, except with five hpothesis steps. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ 𝜏    &   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ 𝜂
Theorem	eel11111 44695	Five-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc 1384 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	e12 44696	A virtual deduction elimination rule (see sylsyld 61). (Contributed by Alan Sare, 21-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜓 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )
Theorem	e12an 44697	Conjunction form of e12 44696 (see syl6an 684). (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )
Theorem	el12 44698	Virtual deduction form of syl2an 596. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜏   ▶   𝜒   )    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   (   𝜑   ,   𝜏   )   ▶   𝜃   )
Theorem	e20 44699	A virtual deduction elimination rule (see syl6mpi 67). (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (𝜒 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	e20an 44700	Conjunction form of e20 44699. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )