Theorem sbc3orgVD 42360

Description: Virtual deduction proof of the analogue of sbcor 3764 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 42136	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
3::	⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))
32:3:	⊢ ∀𝑥(((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))
33:1,32,?: e10 42203	⊢ (   𝐴 ∈ 𝐵   ▶   [𝐴 / 𝑥](((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))   )
4:1,33,?: e11 42197	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒))   )
5:2,4,?: e11 42197	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
6:1,?: e1a 42136	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓))   )
7:6,?: e1a 42136	⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
8:5,7,?: e11 42197	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
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
sbc3orgVD	⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒)))

Proof of Theorem sbc3orgVD

Step	Hyp	Ref	Expression
1		idn1 42083	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2		sbcor 3764	. . . . . . 7 ⊢ ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))
3	2	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒)))
4	1, 3	e1a 42136	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
5		df-3or 1086	. . . . . . . . 9 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))
6	5	bicomi 223	. . . . . . . 8 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))
7	6	ax-gen 1799	. . . . . . 7 ⊢ ∀𝑥(((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))
8		spsbc 3724	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒)) → [𝐴 / 𝑥](((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))))
9	1, 7, 8	e10 42203	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   [𝐴 / 𝑥](((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒))   )
10		sbcbig 3765	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒)) ↔ ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒))))
11	10	biimpd 228	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ 𝜓 ∨ 𝜒)) → ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒))))
12	1, 9, 11	e11 42197	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒))   )
13		bitr3 352	. . . . . 6 ⊢ (([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒)) → (([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))))
14	13	com12 32	. . . . 5 ⊢ (([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒)) → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))))
15	4, 12, 14	e11 42197	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
16		sbcor 3764	. . . . . . 7 ⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓))
17	16	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓)))
18	1, 17	e1a 42136	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓))   )
19		orbi1 914	. . . . 5 ⊢ (([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓)) → (([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)))
20	18, 19	e1a 42136	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
21		bibi1 351	. . . . 5 ⊢ (([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)) ↔ (([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))))
22	21	biimprd 247	. . . 4 ⊢ (([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒)) → ((([𝐴 / 𝑥](𝜑 ∨ 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))))
23	15, 20, 22	e11 42197	. . 3 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
24		df-3or 1086	. . . 4 ⊢ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))
25	24	bicomi 223	. . 3 ⊢ ((([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))
26		bibi1 351	. . . 4 ⊢ (([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒)) ↔ ((([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))))
27	26	biimprd 247	. . 3 ⊢ (([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)) → (((([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))))
28	23, 25, 27	e10 42203	. 2 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))   )
29	28	in1 42080	1 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒)))

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 843   ∨ w3o 1084  ∀wal 1537   ∈ wcel 2108  [wsbc 3711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-sbc 3712  df-vd1 42079

This theorem is referenced by: (None)