Theorem orbi1rVD 16672

Description: Virtual deduction proof of orbi1r 1282. 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::	|- . (ph <-> ps)   ⊢   (ph <-> ps) .
2::	|- . (ph <-> ps), (ch \/ ph)    ⊢   (ch \/ ph) .
3:2,?: e2 16521	|- . (ph <-> ps), (ch \/ ph)    ⊢   (ph \/ ch) .
4:1,3,?: e12 16593	|- . (ph <-> ps), (ch \/ ph)    ⊢   (ps \/ ch) .
5:4,?: e2 16521	|- . (ph <-> ps), (ch \/ ph)    ⊢   (ch \/ ps) .
6:5:	|- . (ph <-> ps)   ⊢   ((ch \/ ph) -> (ch \/ ps)) .
7::	|- . (ph <-> ps), (ch \/ ps)    ⊢   (ch \/ ps) .
8:7,?: e2 16521	|- . (ph <-> ps), (ch \/ ps)    ⊢   (ps \/ ch) .
9:1,8,?: e12 16593	|- . (ph <-> ps), (ch \/ ps)    ⊢   (ph \/ ch) .
10:9,?: e2 16521	|- . (ph <-> ps), (ch \/ ps)    ⊢   (ch \/ ph) .
11:10:	|- . (ph <-> ps)   ⊢   ((ch \/ ps) -> (ch \/ ph)) .
12:6,11,?: e11 16578	|- . (ph <-> ps)   ⊢   ((ch \/ ph) <-> (ch \/ ps)) .
qed:12:	|- ((ph <-> ps) -> ((ch \/ ph) <-> (ch \/ ps)))

Assertion

Ref	Expression
orbi1rVD	|- ((ph <-> ps) -> ((ch \/ ph) <-> (ch \/ ps)))

Proof of Theorem orbi1rVD

Step	Hyp	Ref	Expression
1		idn1 16484	. . . . . 6 |- . (ph <-> ps)   ⊢   (ph <-> ps) .
2		idn2 16509	. . . . . . 7 |- . (ph <-> ps), (ch \/ ph)   ⊢   (ch \/ ph) .
3		pm1.4 267	. . . . . . 7 |- ((ch \/ ph) -> (ph \/ ch))
4	2, 3	e2 16521	. . . . . 6 |- . (ph <-> ps), (ch \/ ph)   ⊢   (ph \/ ch) .
5		orbi1 682	. . . . . . 7 |- ((ph <-> ps) -> ((ph \/ ch) <-> (ps \/ ch)))
6	5	biimpd 170	. . . . . 6 |- ((ph <-> ps) -> ((ph \/ ch) -> (ps \/ ch)))
7	1, 4, 6	e12 16593	. . . . 5 |- . (ph <-> ps), (ch \/ ph)   ⊢   (ps \/ ch) .
8		pm1.4 267	. . . . 5 |- ((ps \/ ch) -> (ch \/ ps))
9	7, 8	e2 16521	. . . 4 |- . (ph <-> ps), (ch \/ ph)   ⊢   (ch \/ ps) .
10	9	in2 16506	. . 3 |- . (ph <-> ps)   ⊢   ((ch \/ ph) -> (ch \/ ps)) .
11		idn2 16509	. . . . . . 7 |- . (ph <-> ps), (ch \/ ps)   ⊢   (ch \/ ps) .
12		pm1.4 267	. . . . . . 7 |- ((ch \/ ps) -> (ps \/ ch))
13	11, 12	e2 16521	. . . . . 6 |- . (ph <-> ps), (ch \/ ps)   ⊢   (ps \/ ch) .
14	5	biimprd 171	. . . . . 6 |- ((ph <-> ps) -> ((ps \/ ch) -> (ph \/ ch)))
15	1, 13, 14	e12 16593	. . . . 5 |- . (ph <-> ps), (ch \/ ps)   ⊢   (ph \/ ch) .
16		pm1.4 267	. . . . 5 |- ((ph \/ ch) -> (ch \/ ph))
17	15, 16	e2 16521	. . . 4 |- . (ph <-> ps), (ch \/ ps)   ⊢   (ch \/ ph) .
18	17	in2 16506	. . 3 |- . (ph <-> ps)   ⊢   ((ch \/ ps) -> (ch \/ ph)) .
19		bi3 167	. . 3 |- (((ch \/ ph) -> (ch \/ ps)) -> (((ch \/ ps) -> (ch \/ ph)) -> ((ch \/ ph) <-> (ch \/ ps))))
20	10, 18, 19	e11 16578	. 2 |- . (ph <-> ps)   ⊢   ((ch \/ ph) <-> (ch \/ ps)) .
21	20	in1 16481	1 |- ((ph <-> ps) -> ((ch \/ ph) <-> (ch \/ ps)))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239

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

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-vd1 16480  df-vd2 16489

Copyright terms: Public domain