Theorem sbc3orgVD 42801

Description: Virtual deduction proof of the analogue of sbcor 3780 with three disjuncts. 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 42577	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
3::	⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))
32:3:	⊢ ∀𝑥(((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))
33:1,32,?: e10 42644	⊢ (   𝐴 ∈ 𝐵   ▶   [𝐴 / 𝑥](((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))   )
4:1,33,?: e11 42638	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒))   )
5:2,4,?: e11 42638	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
6:1,?: e1a 42577	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓))   )
7:6,?: e1a 42577	⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
8:5,7,?: e11 42638	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
9:?:	⊢ ((([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))
10:8,9,?: e10 42644	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))   )
qed:10:	⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒)))

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

Assertion

Ref	Expression
sbc3orgVD	⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒)))

Proof of Theorem sbc3orgVD

Step	Hyp	Ref	Expression
1		idn1 42524	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2		sbcor 3780	. . . . . . 7 ⊢ ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))
3	2	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒)))
4	1, 3	e1a 42577	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
5		df-3or 1087	. . . . . . . . 9 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
6	5	bicomi 223	. . . . . . . 8 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))
7	6	ax-gen 1796	. . . . . . 7 ⊢ ∀𝑥(((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))
8		spsbc 3740	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒)) → [𝐴 / 𝑥](((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))))
9	1, 7, 8	e10 42644	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   [𝐴 / 𝑥](((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))   )
10		sbcbig 3781	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒)) ↔ ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒))))
11	10	biimpd 228	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒)) → ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒))))
12	1, 9, 11	e11 42638	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒))   )
13		bitr3 352	. . . . . 6 ⊢ (([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒)) → (([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))))
14	13	com12 32	. . . . 5 ⊢ (([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒)) → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))))
15	4, 12, 14	e11 42638	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
16		sbcor 3780	. . . . . . 7 ⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓))
17	16	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓)))
18	1, 17	e1a 42577	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓))   )
19		orbi1 915	. . . . 5 ⊢ (([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓)) → (([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)))
20	18, 19	e1a 42577	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
21		bibi1 351	. . . . 5 ⊢ (([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)) ↔ (([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))))
22	21	biimprd 247	. . . 4 ⊢ (([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒)) → ((([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))))
23	15, 20, 22	e11 42638	. . 3 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
24		df-3or 1087	. . . 4 ⊢ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))
25	24	bicomi 223	. . 3 ⊢ ((([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))
26		bibi1 351	. . . 4 ⊢ (([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒)) ↔ ((([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))))
27	26	biimprd 247	. . 3 ⊢ (([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)) → (((([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))))
28	23, 25, 27	e10 42644	. 2 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))   )
29	28	in1 42521	1 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒)))

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 844   ∨ w3o 1085  ∀wal 1538   ∈ wcel 2105  [wsbc 3727

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2170  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-tru 1543  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-sbc 3728  df-vd1 42520

This theorem is referenced by: (None)