Theorem orbi1rVD 45830

Description: Virtual deduction proof of orbi1r 45493. 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 45614	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)    ▶   (𝜑 ∨ 𝜒)   )
4:1,3,?: e12 45706	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)    ▶   (𝜓 ∨ 𝜒)   )
5:4,?: e2 45614	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)    ▶   (𝜒 ∨ 𝜓)   )
6:5:	⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))   )
7::	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)    ▶   (𝜒 ∨ 𝜓)   )
8:7,?: e2 45614	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)    ▶   (𝜓 ∨ 𝜒)   )
9:1,8,?: e12 45706	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)    ▶   (𝜑 ∨ 𝜒)   )
10:9,?: e2 45614	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)    ▶   (𝜒 ∨ 𝜑)   )
11:10:	⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑))   )
12:6,11,?: e11 45671	⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))   )
qed:12:	⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)))

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

Assertion

Ref	Expression
orbi1rVD	⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)))

Proof of Theorem orbi1rVD

Step	Hyp	Ref	Expression
1		idn1 45557	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ▶   (𝜑 ↔ 𝜓)   )
2		idn2 45596	. . . . . . 7 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)   ▶   (𝜒 ∨ 𝜑)   )
3		pm1.4 883	. . . . . . 7 ⊢ ((𝜒 ∨ 𝜑) → (𝜑 ∨ 𝜒))
4	2, 3	e2 45614	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)   ▶   (𝜑 ∨ 𝜒)   )
5		orbi1 931	. . . . . . 7 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)))
6	5	biimpd 232	. . . . . 6 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜒)))
7	1, 4, 6	e12 45706	. . . . 5 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)   ▶   (𝜓 ∨ 𝜒)   )
8		pm1.4 883	. . . . 5 ⊢ ((𝜓 ∨ 𝜒) → (𝜒 ∨ 𝜓))
9	7, 8	e2 45614	. . . 4 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)   ▶   (𝜒 ∨ 𝜓)   )
10	9	in2 45588	. . 3 ⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))   )
11		idn2 45596	. . . . . . 7 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)   ▶   (𝜒 ∨ 𝜓)   )
12		pm1.4 883	. . . . . . 7 ⊢ ((𝜒 ∨ 𝜓) → (𝜓 ∨ 𝜒))
13	11, 12	e2 45614	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)   ▶   (𝜓 ∨ 𝜒)   )
14	5	biimprd 251	. . . . . 6 ⊢ ((𝜑 ↔ 𝜓) → ((𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜒)))
15	1, 13, 14	e12 45706	. . . . 5 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)   ▶   (𝜑 ∨ 𝜒)   )
16		pm1.4 883	. . . . 5 ⊢ ((𝜑 ∨ 𝜒) → (𝜒 ∨ 𝜑))
17	15, 16	e2 45614	. . . 4 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)   ▶   (𝜒 ∨ 𝜑)   )
18	17	in2 45588	. . 3 ⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑))   )
19		impbi 211	. . 3 ⊢ (((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) → (((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑)) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))))
20	10, 18, 19	e11 45671	. 2 ⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))   )
21	20	in1 45554	1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-vd1 45553  df-vd2 45561

This theorem is used by: (None)