P. 453 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

e31 45201

A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )

Theorem

ee31 45202

e31 45201 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))

Theorem

e31an 45203

A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ▶   𝜏   )    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )

Theorem

ee31an 45204

e31an 45203 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))

Theorem

e23 45205

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 45206

A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜂   )

Theorem

ee23an 45207

e23an 45206 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    &   ⊢ ((𝜒 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))

Theorem

e32 45208

A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )

Theorem

ee32 45209

e32 45208 without virtual deductions. (Contributed by Alan Sare, 18-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))

Theorem

e32an 45210

A virtual deduction elimination rule. (Contributed by Alan Sare, 24-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )

Theorem

ee32an 45211

e33an 45185 without virtual deductions. (Contributed by Alan Sare, 14-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ ((𝜃 ∧ 𝜏) → 𝜂)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))

Theorem

e123 45212

A virtual deduction elimination rule. (Contributed by Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜑   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜒   ,   𝜏   ▶   𝜂   )    &   ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜒   ,   𝜏   ▶   𝜁   )

Theorem

ee123 45213

e123 45212 without virtual deductions. (Contributed by Alan Sare, 25-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂)))    &   ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜁)))

Theorem

el123 45214

A virtual deduction elimination rule. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   𝜑   ▶   𝜓   )    &   ⊢ (   𝜒   ▶   𝜃   )    &   ⊢ (   𝜏   ▶   𝜂   )    &   ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)    ⇒   ⊢ (   (   𝜑   ,   𝜒   ,   𝜏   )   ▶   𝜁   )

Theorem

e233 45215

A virtual deduction elimination rule. (Contributed by Alan Sare, 29-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   𝜑   ,   𝜓   ▶   𝜒   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜏   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜂   )    &   ⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜃   ▶   𝜁   )

Theorem

e323 45216

A virtual deduction elimination rule. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜃   )    &   ⊢ (   𝜑   ,   𝜓   ▶   𝜏   )    &   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜂   )    &   ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (   𝜑   ,   𝜓   ,   𝜒   ▶   𝜁   )

Theorem

e000 45217

A virtual deduction elimination rule. The non-virtual deduction form of e000 45217 is the virtual deduction form. (Contributed by Alan Sare, 14-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ 𝜒    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ 𝜃

Theorem

e00 45218

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.)

⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ 𝜒

Theorem

e00an 45219

Elimination rule identical to mp2an 698. The non-virtual deduction form is the virtual deduction form, which is mp2an 698. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒

Theorem

eel00cT 45220

An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝜑    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (⊤ → 𝜒)

Theorem

eelTT 45221

An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (⊤ → 𝜑)    &   ⊢ (⊤ → 𝜓)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒

Theorem

e0a 45222

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.)

⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓

Theorem

eelT 45223

An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (⊤ → 𝜑)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓

Theorem

eel0cT 45224

An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (⊤ → 𝜓)

Theorem

eelT0 45225

An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (⊤ → 𝜑)    &   ⊢ 𝜓    &   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ 𝜒

Theorem

e0bi 45226

Elimination rule identical to mpbi 231. The non-virtual deduction form is the virtual deduction form, which is mpbi 231. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝜑    &   ⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ 𝜓

Theorem

e0bir 45227

Elimination rule identical to mpbir 232. The non-virtual deduction form is the virtual deduction form, which is mpbir 232. (Contributed by Alan Sare, 15-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝜑    &   ⊢ (𝜓 ↔ 𝜑)    ⇒   ⊢ 𝜓

Theorem

uun0.1 45228

Convention notation form of un0.1 45229. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (⊤ → 𝜑)    &   ⊢ (𝜓 → 𝜒)    &   ⊢ ((⊤ ∧ 𝜓) → 𝜃)    ⇒   ⊢ (𝜓 → 𝜃)

Theorem

un0.1 45229

⊤ is the constant true, a tautology (see df-tru 1550). Kleene's "empty conjunction" is logically equivalent to ⊤. In a virtual deduction we shall interpret ⊤ to be the empty wff or the empty collection of virtual hypotheses. ⊤ in a virtual deduction translated into conventional notation we shall interpret to be Kleene's empty conjunction. If 𝜃 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.)

⊢ (   ⊤   ▶   𝜑   )    &   ⊢ (   𝜓   ▶   𝜒   )    &   ⊢ (   (   ⊤   ,   𝜓   )   ▶   𝜃   )    ⇒   ⊢ (   𝜓   ▶   𝜃   )

Theorem

uunT1 45230

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 3-Dec-2015.) Proof was revised to accommodate a possible future version of df-tru 1550. (Revised by David A. Wheeler, 8-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((⊤ ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)

Theorem

uunT1p1 45231

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.)

⊢ ((𝜑 ∧ ⊤) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)

Theorem

uunT21 45232

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.)

⊢ ((⊤ ∧ (𝜑 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

uun121 45233

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.)

⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

uun121p1 45234

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.)

⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

uun132 45235

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.)

⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

uun132p1 45236

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.)

⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

anabss7p1 45237

A deduction unionizing a non-unionized collection of virtual hypotheses. This would have been named uun221 if the zeroth permutation did not exist in set.mm as anabss7 679. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (((𝜓 ∧ 𝜑) ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Theorem

un10 45238

A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   (   𝜑   ,   ⊤   )   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ▶   𝜓   )

Theorem

un01 45239

A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   (   ⊤   ,   𝜑   )   ▶   𝜓   )    ⇒   ⊢ (   𝜑   ▶   𝜓   )

Theorem

un2122 45240

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.)

⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

uun2131 45241

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.)

⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

uun2131p1 45242

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.)

⊢ (((𝜑 ∧ 𝜒) ∧ (𝜑 ∧ 𝜓)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

uunTT1 45243

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.)

⊢ ((⊤ ∧ ⊤ ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)

Theorem

uunTT1p1 45244

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.)

⊢ ((⊤ ∧ 𝜑 ∧ ⊤) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)

Theorem

uunTT1p2 45245

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.)

⊢ ((𝜑 ∧ ⊤ ∧ ⊤) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)

Theorem

uunT11 45246

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.)

⊢ ((⊤ ∧ 𝜑 ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)

Theorem

uunT11p1 45247

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.)

⊢ ((𝜑 ∧ ⊤ ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)

Theorem

uunT11p2 45248

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.)

⊢ ((𝜑 ∧ 𝜑 ∧ ⊤) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)

Theorem

uunT12 45249

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.)

⊢ ((⊤ ∧ 𝜑 ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

uunT12p1 45250

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.)

⊢ ((⊤ ∧ 𝜓 ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

uunT12p2 45251

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.)

⊢ ((𝜑 ∧ ⊤ ∧ 𝜓) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

uunT12p3 45252

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.)

⊢ ((𝜓 ∧ ⊤ ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

uunT12p4 45253

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.)

⊢ ((𝜑 ∧ 𝜓 ∧ ⊤) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

uunT12p5 45254

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.)

⊢ ((𝜓 ∧ 𝜑 ∧ ⊤) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

uun111 45255

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.)

⊢ ((𝜑 ∧ 𝜑 ∧ 𝜑) → 𝜓)    ⇒   ⊢ (𝜑 → 𝜓)

Theorem

3anidm12p1 45256

A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1427 denotes the deduction which would have been named uun112 if it did not pre-exist in set.mm. This second permutation's name is based on this pre-existing name. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

3anidm12p2 45257

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.)

⊢ ((𝜓 ∧ 𝜑 ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

uun123 45258

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.)

⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

uun123p1 45259

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.)

⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

uun123p2 45260

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.)

⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

uun123p3 45261

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.)

⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

uun123p4 45262

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.)

⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

uun2221 45263

A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 30-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝜑 ∧ 𝜑 ∧ (𝜓 ∧ 𝜑)) → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Theorem

uun2221p1 45264

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.)

⊢ ((𝜑 ∧ (𝜓 ∧ 𝜑) ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Theorem

uun2221p2 45265

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.)

⊢ (((𝜓 ∧ 𝜑) ∧ 𝜑 ∧ 𝜑) → 𝜒)    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Theorem

3impdirp1 45266

A deduction unionizing a non-unionized collection of virtual hypotheses. Commuted version of 3impdir 1358. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (((𝜒 ∧ 𝜓) ∧ (𝜑 ∧ 𝜓)) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)

Theorem

3impcombi 45267

A 1-hypothesis propositional calculus deduction. (Contributed by Alan Sare, 25-Sep-2017.)

⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

21.41.6  Theorems proved using Virtual Deduction

Theorem

trsspwALT 45268

Virtual deduction proof of the left-to-right implication of dftr4 5192. A transitive class is a subset of its power class. This proof corresponds to the virtual deduction proof of dftr4 5192 without accumulating results. (Contributed by Alan Sare, 29-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴)

Theorem

trsspwALT2 45269

Virtual deduction proof of trsspwALT 45268. This proof is the same as the proof of trsspwALT 45268 except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A transitive class is a subset of its power class. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴)

Theorem

trsspwALT3 45270

Short predicate calculus proof of the left-to-right implication of dftr4 5192. A transitive class is a subset of its power class. This proof was constructed by applying Metamath's minimize command to the proof of trsspwALT2 45269, which is the virtual deduction proof trsspwALT 45268 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴)

Theorem

sspwtr 45271

Virtual deduction proof of the right-to-left implication of dftr4 5192. A class which is a subclass of its power class is transitive. This proof corresponds to the virtual deduction proof of sspwtr 45271 without accumulating results. (Contributed by Alan Sare, 2-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴)

Theorem

sspwtrALT 45272

Virtual deduction proof of sspwtr 45271. This proof is the same as the proof of sspwtr 45271 except each virtual deduction symbol is replaced by its non-virtual deduction symbol equivalent. A class which is a subclass of its power class is transitive. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴)

Theorem

sspwtrALT2 45273

Short predicate calculus proof of the right-to-left implication of dftr4 5192. A class which is a subclass of its power class is transitive. This proof was constructed by applying Metamath's minimize command to the proof of sspwtrALT 45272, which is the virtual deduction proof sspwtr 45271 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴)

Theorem

pwtrVD 45274

Virtual deduction proof of pwtr 5398; see pwtrrVD 45275 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (Tr 𝐴 → Tr 𝒫 𝐴)

Theorem

pwtrrVD 45275

Virtual deduction proof of pwtr 5398; see pwtrVD 45274 for the converse. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝐴 ∈ V    ⇒   ⊢ (Tr 𝒫 𝐴 → Tr 𝐴)

Theorem

suctrALT 45276

The successor of a transitive class is transitive. The proof of https://us.metamath.org/other/completeusersproof/suctrvd.html is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctrALT 45276 using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/suctrro.html 45276 is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. See suctr 6405 for the original proof. (Contributed by Alan Sare, 11-Apr-2009.) (Revised by Alan Sare, 12-Jun-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (Tr 𝐴 → Tr suc 𝐴)

Theorem

snssiALTVD 45277

Virtual deduction proof of snssiALT 45278. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

Theorem

snssiALT 45278

If a class is an element of another class, then its singleton is a subclass of that other class. Alternate proof of snssi 4724. This theorem was automatically generated from snssiALTVD 45277 using a translation program. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

Theorem

snsslVD 45279

Virtual deduction proof of snssl 45280. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝐴 ∈ V    ⇒   ⊢ ({𝐴} ⊆ 𝐵 → 𝐴 ∈ 𝐵)

Theorem

snssl 45280

If a singleton is a subclass of another class, then the singleton's element is an element of that other class. This theorem is the right-to-left implication of the biconditional snss 4723. The proof of this theorem was automatically generated from snsslVD 45279 using a tools command file, translateMWO.cmd, by translating the proof into its non-virtual deduction form and minimizing it. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝐴 ∈ V    ⇒   ⊢ ({𝐴} ⊆ 𝐵 → 𝐴 ∈ 𝐵)

Theorem

snelpwrVD 45281

Virtual deduction proof of snelpwi 5390. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Theorem

unipwrVD 45282

Virtual deduction proof of unipwr 45283. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝐴 ⊆ ∪ 𝒫 𝐴

Theorem

unipwr 45283

A class is a subclass of the union of its power class. This theorem is the right-to-left subclass lemma of unipw 5396. The proof of this theorem was automatically generated from unipwrVD 45282 using a tools command file , translateMWO.cmd , by translating the proof into its non-virtual deduction form and minimizing it. (Contributed by Alan Sare, 25-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝐴 ⊆ ∪ 𝒫 𝐴

Theorem

sstrALT2VD 45284

Virtual deduction proof of sstrALT2 45285. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

Theorem

sstrALT2 45285

Virtual deduction proof of sstr 3930, transitivity of subclasses, Theorem 6 of [Suppes] p. 23. This theorem was automatically generated from sstrALT2VD 45284 using the command file translate_without_overwriting.cmd . It was not minimized because the automated minimization excluding duplicates generates a minimized proof which, although not directly containing any duplicates, indirectly contains a duplicate. That is, the trace back of the minimized proof contains a duplicate. This is undesirable because some step(s) of the minimized proof use the proven theorem. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

Theorem

suctrALT2VD 45286

Virtual deduction proof of suctrALT2 45287. (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (Tr 𝐴 → Tr suc 𝐴)

Theorem

suctrALT2 45287

Virtual deduction proof of suctr 6405. The successor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD 45286 using the tools command file translate_without_overwriting_minimize_excluding_duplicates.cmd . (Contributed by Alan Sare, 11-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (Tr 𝐴 → Tr suc 𝐴)

Theorem

elex2VD 45288*

Virtual deduction proof of elex2 2817. (Contributed by Alan Sare, 25-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Theorem

elex22VD 45289*

Virtual deduction proof of elex22 3457. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))

Theorem

eqsbc2VD 45290*

Virtual deduction proof of eqsbc2 3793. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴))

Theorem

zfregs2VD 45291*

Virtual deduction proof of zfregs2 9652. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ≠ ∅ → ¬ ∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥))

Theorem

tpid3gVD 45292

Virtual deduction proof of tpid3g 4711. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴})

Theorem

en3lplem1VD 45293*

Virtual deduction proof of en3lplem1 9531. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)))

Theorem

en3lplem2VD 45294*

Virtual deduction proof of en3lplem2 9532. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥)))

Theorem

en3lpVD 45295

Virtual deduction proof of en3lp 9533. (Contributed by Alan Sare, 24-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴)

21.41.7  Theorems proved using Virtual Deduction with mmj2 assistance

Theorem

simplbi2VD 45296

Virtual deduction proof of simplbi2 501. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

h1::	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
3:1,?: e0a 45222	⊢ ((𝜓 ∧ 𝜒) → 𝜑)
qed:3,?: e0a 45222	⊢ (𝜓 → (𝜒 → 𝜑))

The proof of simplbi2 501 was automatically derived from it. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (𝜓 → (𝜒 → 𝜑))

Theorem

3ornot23VD 45297

Virtual deduction proof of 3ornot23 44960. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   (¬ 𝜑 ∧ ¬ 𝜓)   )
2::	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   (𝜒 ∨ 𝜑 ∨ 𝜓)   )
3:1,?: e1a 45078	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ¬ 𝜑   )
4:1,?: e1a 45078	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ¬ 𝜓   )
5:3,4,?: e11 45139	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ¬ (𝜑 ∨ 𝜓)   )
6:2,?: e2 45082	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   (𝜒 ∨ (𝜑 ∨ 𝜓))   )
7:5,6,?: e12 45174	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ,   (𝜒 ∨ 𝜑 ∨ 𝜓)   ▶   𝜒   )
8:7:	⊢ (   (¬ 𝜑 ∧ ¬ 𝜓)   ▶   ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒)   )
qed:8:	⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒))

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒))

Theorem

orbi1rVD 45298

Virtual deduction proof of orbi1r 44961. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	⊢ (   (𝜑 ↔ 𝜓)   ▶   (𝜑 ↔ 𝜓)   )
2::	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)    ▶   (𝜒 ∨ 𝜑)   )
3:2,?: e2 45082	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)    ▶   (𝜑 ∨ 𝜒)   )
4:1,3,?: e12 45174	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)    ▶   (𝜓 ∨ 𝜒)   )
5:4,?: e2 45082	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)    ▶   (𝜒 ∨ 𝜓)   )
6:5:	⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))   )
7::	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)    ▶   (𝜒 ∨ 𝜓)   )
8:7,?: e2 45082	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)    ▶   (𝜓 ∨ 𝜒)   )
9:1,8,?: e12 45174	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)    ▶   (𝜑 ∨ 𝜒)   )
10:9,?: e2 45082	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)    ▶   (𝜒 ∨ 𝜑)   )
11:10:	⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑))   )
12:6,11,?: e11 45139	⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))   )
qed:12:	⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)))

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)))

Theorem

bitr3VD 45299

Virtual deduction proof of bitr3 353. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	⊢ (   (𝜑 ↔ 𝜓)   ▶   (𝜑 ↔ 𝜓)   )
2:1,?: e1a 45078	⊢ (   (𝜑 ↔ 𝜓)   ▶   (𝜓 ↔ 𝜑)   )
3::	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜑 ↔ 𝜒)    ▶   (𝜑 ↔ 𝜒)   )
4:3,?: e2 45082	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜑 ↔ 𝜒)    ▶   (𝜒 ↔ 𝜑)   )
5:2,4,?: e12 45174	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜑 ↔ 𝜒)    ▶   (𝜓 ↔ 𝜒)   )
6:5:	⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜑 ↔ 𝜒) → (𝜓 ↔ 𝜒))   )
qed:6:	⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) → (𝜓 ↔ 𝜒)))

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) → (𝜓 ↔ 𝜒)))

Theorem

3orbi123VD 45300

Virtual deduction proof of 3orbi123 44962. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   )
2:1,?: e1a 45078	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   (𝜑 ↔ 𝜓)   )
3:1,?: e1a 45078	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   (𝜒 ↔ 𝜃)   )
4:1,?: e1a 45078	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   (𝜏 ↔ 𝜂)   )
5:2,3,?: e11 45139	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))   )
6:5,4,?: e11 45139	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))   )
7:?:	⊢ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ (𝜑 ∨ 𝜒 ∨ 𝜏))
8:6,7,?: e10 45145	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))   )
9:?:	⊢ (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))
10:8,9,?: e10 45145	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))   )
qed:10:	⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)))

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)))