Theorem 3orbi123VD 16674

Description: Virtual deduction proof of 3orbi123 1284. 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) /\ (ch <-> th) /\ (ta <-> et))   ⊢   ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et)) .
2:1,?: e1_ 16518	|- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   (ph <-> ps) .
3:1,?: e1_ 16518	|- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   (ch <-> th) .
4:1,?: e1_ 16518	|- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   (ta <-> et) .
5:2,3,?: e11 16578	|- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   ((ph \/ ch) <-> (ps \/ th)) .
6:5,4,?: e11 16578	|- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   (((ph \/ ch) \/ ta) <-> ((ps \/ th) \/ et)) .
7:?:	|- (((ph \/ ch) \/ ta) <-> (ph \/ ch \/ ta))
8:6,7,?: e10 16585	|- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   ((ph \/ ch \/ ta) <-> ((ps \/ th) \/ et)) .
9:?:	|- (((ps \/ th) \/ et) <-> (ps \/ th \/ et))
10:8,9,?: e10 16585	|- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   ((ph \/ ch \/ ta) <-> (ps \/ th \/ et)) .
qed:10:	|- (((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et)) -> ((ph \/ ch \/ ta) <-> (ps \/ th \/ et)))

Assertion

Ref	Expression
3orbi123VD	|- (((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et)) -> ((ph \/ ch \/ ta) <-> (ps \/ th \/ et)))

Proof of Theorem 3orbi123VD

Step	Hyp	Ref	Expression
1		idn1 16484	. . . . . . 7 |- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et)) .
2		simp1 876	. . . . . . 7 |- (((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et)) -> (ph <-> ps))
3	1, 2	e1_ 16518	. . . . . 6 |- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   (ph <-> ps) .
4		simp2 877	. . . . . . 7 |- (((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et)) -> (ch <-> th))
5	1, 4	e1_ 16518	. . . . . 6 |- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   (ch <-> th) .
6		pm4.39 692	. . . . . . 7 |- (((ph <-> ps) /\ (ch <-> th)) -> ((ph \/ ch) <-> (ps \/ th)))
7	6	ex 402	. . . . . 6 |- ((ph <-> ps) -> ((ch <-> th) -> ((ph \/ ch) <-> (ps \/ th))))
8	3, 5, 7	e11 16578	. . . . 5 |- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   ((ph \/ ch) <-> (ps \/ th)) .
9		simp3 878	. . . . . 6 |- (((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et)) -> (ta <-> et))
10	1, 9	e1_ 16518	. . . . 5 |- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   (ta <-> et) .
11		pm4.39 692	. . . . . 6 |- ((((ph \/ ch) <-> (ps \/ th)) /\ (ta <-> et)) -> (((ph \/ ch) \/ ta) <-> ((ps \/ th) \/ et)))
12	11	ex 402	. . . . 5 |- (((ph \/ ch) <-> (ps \/ th)) -> ((ta <-> et) -> (((ph \/ ch) \/ ta) <-> ((ps \/ th) \/ et))))
13	8, 10, 12	e11 16578	. . . 4 |- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   (((ph \/ ch) \/ ta) <-> ((ps \/ th) \/ et)) .
14		df-3or 859	. . . . 5 |- ((ph \/ ch \/ ta) <-> ((ph \/ ch) \/ ta))
15	14	bicomi 189	. . . 4 |- (((ph \/ ch) \/ ta) <-> (ph \/ ch \/ ta))
16		bitr3 1283	. . . . 5 |- ((((ph \/ ch) \/ ta) <-> (ph \/ ch \/ ta)) -> ((((ph \/ ch) \/ ta) <-> ((ps \/ th) \/ et)) -> ((ph \/ ch \/ ta) <-> ((ps \/ th) \/ et))))
17	16	com12 14	. . . 4 |- ((((ph \/ ch) \/ ta) <-> ((ps \/ th) \/ et)) -> ((((ph \/ ch) \/ ta) <-> (ph \/ ch \/ ta)) -> ((ph \/ ch \/ ta) <-> ((ps \/ th) \/ et))))
18	13, 15, 17	e10 16585	. . 3 |- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   ((ph \/ ch \/ ta) <-> ((ps \/ th) \/ et)) .
19		df-3or 859	. . . 4 |- ((ps \/ th \/ et) <-> ((ps \/ th) \/ et))
20	19	bicomi 189	. . 3 |- (((ps \/ th) \/ et) <-> (ps \/ th \/ et))
21		bitr 684	. . . 4 |- ((((ph \/ ch \/ ta) <-> ((ps \/ th) \/ et)) /\ (((ps \/ th) \/ et) <-> (ps \/ th \/ et))) -> ((ph \/ ch \/ ta) <-> (ps \/ th \/ et)))
22	21	ex 402	. . 3 |- (((ph \/ ch \/ ta) <-> ((ps \/ th) \/ et)) -> ((((ps \/ th) \/ et) <-> (ps \/ th \/ et)) -> ((ph \/ ch \/ ta) <-> (ps \/ th \/ et))))
23	18, 20, 22	e10 16585	. 2 |- . ((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et))   ⊢   ((ph \/ ch \/ ta) <-> (ps \/ th \/ et)) .
24	23	in1 16481	1 |- (((ph <-> ps) /\ (ch <-> th) /\ (ta <-> et)) -> ((ph \/ ch \/ ta) <-> (ps \/ th \/ et)))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   \/ w3o 857   /\ w3a 858

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-3or 859  df-3an 860  df-vd1 16480

Copyright terms: Public domain