P. 442 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44101-44200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ee201 44101	e201 44100 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜃    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))
Theorem	e120 44102	A virtual deduction elimination rule. (Contributed by Alan Sare, 10-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜂   )
Theorem	ee120 44103	Virtual deduction rule e120 44102 without virtual deduction symbols. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ 𝜏    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜂))
Theorem	e021 44104	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜓   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee021 44105	e021 44104 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ (𝜓 → 𝜏)    &   ⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜒 → 𝜂))
Theorem	e012 44106	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜓   ,   𝜃   ▶   𝜂   )
Theorem	ee012 44107	e012 44106 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → (𝜃 → 𝜏))    &   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜓 → (𝜃 → 𝜂))
Theorem	e102 44108	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ (   𝜑   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (   𝜑   ,   𝜃   ▶   𝜂   )
Theorem	ee102 44109	e102 44108 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ (𝜑 → (𝜃 → 𝜏))    &   ⊢ (𝜓 → (𝜒 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜃 → 𝜂))
Theorem	e22 44110	A virtual deduction elimination rule. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ (𝜒 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	e22an 44111	Conjunction form of e22 44110. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜃   )    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	ee22an 44112	e22an 44111 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜏))
Theorem	e111 44113	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 44114	A virtual deduction elimination rule. (Contributed by Alan Sare, 6-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))    ⇒   ⊢ (   𝜑   ▶   𝜂   )
Theorem	e110 44115	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee110 44116	e110 44115 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e101 44117	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee101 44118	e101 44117 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e011 44119	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (   𝜓   ▶   𝜃   )    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜓   ▶   𝜏   )
Theorem	ee011 44120	e011 44119 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	e100 44121	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜑   ▶   𝜏   )
Theorem	ee100 44122	e100 44121 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜑 → 𝜏)
Theorem	e010 44123	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜓   ▶   𝜏   )
Theorem	ee010 44124	e010 44123 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    &   ⊢ 𝜃    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	e001 44125	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (   𝜒   ▶   𝜃   )    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    ⇒   ⊢ (   𝜒   ▶   𝜏   )
Theorem	ee001 44126	e001 44125 without virtual deductions. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	e11 44127	A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ (𝜓 → (𝜒 → 𝜃))    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	e11an 44128	Conjunction form of e11 44127. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ▶   𝜒   )    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	ee11an 44129	e11an 44128 without virtual deductions. syl22anc 838 is also e11an 44128 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 44130	A virtual deduction elimination rule. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (𝜑 → (𝜒 → 𝜃))    ⇒   ⊢ (   𝜓   ▶   𝜃   )
Theorem	e01an 44131	Conjunction form of e01 44130. (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   𝜓   ▶   𝜃   )
Theorem	ee01an 44132	e01an 44131 without virtual deductions. sylancr 586 is also a form of e01an 44131 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 44133	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 44134	Conjunction form of e10 44133. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ 𝜒    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   𝜑   ▶   𝜃   )
Theorem	ee10an 44135	e10an 44134 without virtual deductions. sylancl 585 is also e10an 44134 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 44136	A virtual deduction elimination rule. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜑 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	e02an 44137	Conjunction form of e02 44136. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	ee02an 44138	e02an 44137 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → 𝜃))    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜓 → (𝜒 → 𝜏))
Theorem	eel021old 44139	el021old 44140 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜓 ∧ 𝜒) → 𝜏)
Theorem	el021old 44140	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   (   𝜓   ,   𝜒   )   ▶   𝜃   )    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   (   𝜓   ,   𝜒   )   ▶   𝜏   )
Theorem	eel132 44141	syl2an 595 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜓 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜂)
Theorem	eel000cT 44142	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (⊤ → 𝜃)
Theorem	eel0TT 44143	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (⊤ → 𝜓)    &   ⊢ (⊤ → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	eelT00 44144	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	eelTTT 44145	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (⊤ → 𝜓)    &   ⊢ (⊤ → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ 𝜃
Theorem	eelT11 44146	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜓 → 𝜏)
Theorem	eelT1 44147	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 44148	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ (𝜃 → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜓 ∧ 𝜃) → 𝜂)
Theorem	eelTT1 44149	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ (⊤ → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	eelT01 44150	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊤ → 𝜑)    &   ⊢ 𝜓    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	eel0T1 44151	An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (⊤ → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜒 → 𝜏)
Theorem	eel12131 44152	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)
Theorem	eel2131 44153	syl2an 595 with antecedents in standard conjunction form. (Contributed by Alan Sare, 26-Aug-2016.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜂)
Theorem	eel3132 44154	syl2an 595 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜂)
Theorem	eel0321old 44155	el0321old 44156 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜂)
Theorem	el0321old 44156	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   (   𝜓   ,   𝜒   ,   𝜃   )   ▶   𝜏   )    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   (   𝜓   ,   𝜒   ,   𝜃   )   ▶   𝜂   )
Theorem	eel2122old 44157	el2122old 44158 without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ (𝜓 → 𝜃)    &   ⊢ (𝜓 → 𝜏)    &   ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜂)
Theorem	el2122old 44158	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   (   𝜑   ,   𝜓   )   ▶   𝜒   )    &   ⊢ (   𝜓   ▶   𝜃   )    &   ⊢ (   𝜓   ▶   𝜏   )    &   ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   (   𝜑   ,   𝜓   )   ▶   𝜂   )
Theorem	eel0000 44159	Elimination rule similar to mp4an 692, except with a left-nested conjunction unification theorem. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)    ⇒   ⊢ 𝜏
Theorem	eel00001 44160	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ (𝜏 → 𝜂)    &   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜏 → 𝜁)
Theorem	eel00000 44161	Elimination rule similar eel0000 44159, except with five hpothesis steps. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ 𝜃    &   ⊢ 𝜏    &   ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)    ⇒   ⊢ 𝜂
Theorem	eel11111 44162	Five-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl113anc 1380 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜑 → 𝜂)    &   ⊢ (((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜁)    ⇒   ⊢ (𝜑 → 𝜁)
Theorem	e12 44163	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 44164	Conjunction form of e12 44163 (see syl6an 683). (Contributed by Alan Sare, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜒   ▶   𝜏   )
Theorem	el12 44165	Virtual deduction form of syl2an 595. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜏   ▶   𝜒   )    &   ⊢ ((𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ (   (   𝜑   ,   𝜏   )   ▶   𝜃   )
Theorem	e20 44166	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 44167	Conjunction form of e20 44166. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ 𝜃    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	ee20an 44168	e20an 44167 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ 𝜃    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜏))
Theorem	e21 44169	A virtual deduction elimination rule (see syl6ci 71). (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ (𝜒 → (𝜃 → 𝜏))    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	e21an 44170	Conjunction form of e21 44169. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ▶   𝜃   )    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )
Theorem	ee21an 44171	e21an 44170 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    &   ⊢ ((𝜒 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜓 → 𝜏))
Theorem	e333 44172	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )    &   ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜁   )
Theorem	e33 44173	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	e33an 44174	Conjunction form of e33 44173. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee33an 44175	e33an 44174 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e3 44176	Meta-connective form of syl8 76. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	e3bi 44177	Biconditional form of e3 44176. syl8ib 256 is e3bi 44177 without virtual deductions. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜃 ↔ 𝜏)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	e3bir 44178	Right biconditional form of e3 44176. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (𝜏 ↔ 𝜃)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜏   )
Theorem	e03 44179	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜑 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜓   ,   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	ee03 44180	e03 44179 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    &   ⊢ (𝜑 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂)))
Theorem	e03an 44181	Conjunction form of e03 44179. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (   𝜓   ,   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜓   ,   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	ee03an 44182	Conjunction form of ee03 44180. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜏)))    &   ⊢ ((𝜑 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜓 → (𝜒 → (𝜃 → 𝜂)))
Theorem	e30 44183	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee30 44184	e30 44183 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ 𝜏    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e30an 44185	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ 𝜏    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee30an 44186	Conjunction form of ee30 44184. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ 𝜏    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e13 44187	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜓 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	e13an 44188	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ,   𝜃   ▶   𝜏   )    &   ⊢ ((𝜓 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜒   ,   𝜃   ▶   𝜂   )
Theorem	ee13an 44189	e13an 44188 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    &   ⊢ ((𝜓 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂)))
Theorem	e31 44190	A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee31 44191	e31 44190 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e31an 44192	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee31an 44193	e31an 44192 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e23 44194	A virtual deduction elimination rule (see syl10 79). (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ (𝜒 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜂   )
Theorem	e23an 44195	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜂   )
Theorem	ee23an 44196	e23an 44195 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))
Theorem	e32 44197	A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee32 44198	e32 44197 without virtual deductions. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))
Theorem	e32an 44199	A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )
Theorem	ee32an 44200	e33an 44174 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))