Theorem orbi1rVD 42468

Description: Virtual deduction proof of orbi1r 42130. 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 42251	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)    ▶   (𝜑 ∨ 𝜒)   )
4:1,3,?: e12 42344	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)    ▶   (𝜓 ∨ 𝜒)   )
5:4,?: e2 42251	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)    ▶   (𝜒 ∨ 𝜓)   )
6:5:	⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))   )
7::	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)    ▶   (𝜒 ∨ 𝜓)   )
8:7,?: e2 42251	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)    ▶   (𝜓 ∨ 𝜒)   )
9:1,8,?: e12 42344	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)    ▶   (𝜑 ∨ 𝜒)   )
10:9,?: e2 42251	⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)    ▶   (𝜒 ∨ 𝜑)   )
11:10:	⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑))   )
12:6,11,?: e11 42308	⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))   )
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 42194	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ▶   (𝜑 ↔ 𝜓)   )
2		idn2 42233	. . . . . . 7 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)   ▶   (𝜒 ∨ 𝜑)   )
3		pm1.4 866	. . . . . . 7 ⊢ ((𝜒 ∨ 𝜑) → (𝜑 ∨ 𝜒))
4	2, 3	e2 42251	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)   ▶   (𝜑 ∨ 𝜒)   )
5		orbi1 915	. . . . . . 7 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)))
6	5	biimpd 228	. . . . . 6 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜒)))
7	1, 4, 6	e12 42344	. . . . 5 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)   ▶   (𝜓 ∨ 𝜒)   )
8		pm1.4 866	. . . . 5 ⊢ ((𝜓 ∨ 𝜒) → (𝜒 ∨ 𝜓))
9	7, 8	e2 42251	. . . 4 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜑)   ▶   (𝜒 ∨ 𝜓)   )
10	9	in2 42225	. . 3 ⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))   )
11		idn2 42233	. . . . . . 7 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)   ▶   (𝜒 ∨ 𝜓)   )
12		pm1.4 866	. . . . . . 7 ⊢ ((𝜒 ∨ 𝜓) → (𝜓 ∨ 𝜒))
13	11, 12	e2 42251	. . . . . 6 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)   ▶   (𝜓 ∨ 𝜒)   )
14	5	biimprd 247	. . . . . 6 ⊢ ((𝜑 ↔ 𝜓) → ((𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜒)))
15	1, 13, 14	e12 42344	. . . . 5 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)   ▶   (𝜑 ∨ 𝜒)   )
16		pm1.4 866	. . . . 5 ⊢ ((𝜑 ∨ 𝜒) → (𝜒 ∨ 𝜑))
17	15, 16	e2 42251	. . . 4 ⊢ (   (𝜑 ↔ 𝜓)   ,   (𝜒 ∨ 𝜓)   ▶   (𝜒 ∨ 𝜑)   )
18	17	in2 42225	. . 3 ⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑))   )
19		impbi 207	. . 3 ⊢ (((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) → (((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑)) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))))
20	10, 18, 19	e11 42308	. 2 ⊢ (   (𝜑 ↔ 𝜓)   ▶   ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))   )
21	20	in1 42191	1 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)))

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-vd1 42190  df-vd2 42198

This theorem is referenced by: (None)