Theorem 3orbi123VD 42359

Description: Virtual deduction proof of 3orbi123 42020. 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 42136	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   (𝜑 ↔ 𝜓)   )
3:1,?: e1a 42136	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   (𝜒 ↔ 𝜃)   )
4:1,?: e1a 42136	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   (𝜏 ↔ 𝜂)   )
5:2,3,?: e11 42197	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))   )
6:5,4,?: e11 42197	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))   )
7:?:	⊢ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ (𝜑 ∨ 𝜒 ∨ 𝜏))
8:6,7,?: e10 42203	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))   )
9:?:	⊢ (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))
10:8,9,?: e10 42203	⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))   )
qed:10:	⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)))

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

Assertion

Ref	Expression
3orbi123VD	⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)))

Proof of Theorem 3orbi123VD

Step	Hyp	Ref	Expression
1		idn1 42083	. . . . . . 7 ⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   )
2		simp1 1134	. . . . . . 7 ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (𝜑 ↔ 𝜓))
3	1, 2	e1a 42136	. . . . . 6 ⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   (𝜑 ↔ 𝜓)   )
4		simp2 1135	. . . . . . 7 ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (𝜒 ↔ 𝜃))
5	1, 4	e1a 42136	. . . . . 6 ⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   (𝜒 ↔ 𝜃)   )
6		pm4.39 973	. . . . . . 7 ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)))
7	6	ex 412	. . . . . 6 ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))))
8	3, 5, 7	e11 42197	. . . . 5 ⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))   )
9		simp3 1136	. . . . . 6 ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → (𝜏 ↔ 𝜂))
10	1, 9	e1a 42136	. . . . 5 ⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   (𝜏 ↔ 𝜂)   )
11		pm4.39 973	. . . . . 6 ⊢ ((((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) ∧ (𝜏 ↔ 𝜂)) → (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)))
12	11	ex 412	. . . . 5 ⊢ (((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) → ((𝜏 ↔ 𝜂) → (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))))
13	8, 10, 12	e11 42197	. . . 4 ⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))   )
14		df-3or 1086	. . . . 5 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜏))
15	14	bicomi 223	. . . 4 ⊢ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ (𝜑 ∨ 𝜒 ∨ 𝜏))
16		bitr3 352	. . . . 5 ⊢ ((((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ (𝜑 ∨ 𝜒 ∨ 𝜏)) → ((((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))))
17	16	com12 32	. . . 4 ⊢ ((((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) → ((((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ (𝜑 ∨ 𝜒 ∨ 𝜏)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))))
18	13, 15, 17	e10 42203	. . 3 ⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))   )
19		df-3or 1086	. . . 4 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))
20	19	bicomi 223	. . 3 ⊢ (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))
21		bitr 801	. . . 4 ⊢ ((((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) ∧ (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)))
22	21	ex 412	. . 3 ⊢ (((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) → ((((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))))
23	18, 20, 22	e10 42203	. 2 ⊢ (   ((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂))   ▶   ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))   )
24	23	in1 42080	1 ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)))

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 843   ∨ w3o 1084   ∧ w3a 1085

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 396  df-or 844  df-3or 1086  df-3an 1087  df-vd1 42079

This theorem is referenced by: (None)