Theorem sbcim2gVD 44873

Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg 3843. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcim2g 44536 is sbcim2gVD 44873 without virtual deductions and was automatically derived from sbcim2gVD 44873.

1::	⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2::	⊢ (   𝐴 ∈ 𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   ▶   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   )
3:1,2:	⊢ (   𝐴 ∈ 𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))   )
4:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   )
5:3,4:	⊢ (   𝐴 ∈ 𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   )
6:5:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))   )
7::	⊢ (   𝐴 ∈ 𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   )
8:4,7:	⊢ (   𝐴 ∈ 𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))   )
9:1:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)))   )
10:8,9:	⊢ (   𝐴 ∈ 𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   ▶   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   )
11:10:	⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)))   )
12:6,11:	⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))   )
qed:12:	⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))

(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Proof of Theorem sbcim2gVD

Step	Hyp	Ref	Expression
1		idn1 44572	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2		idn2 44611	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   ▶   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   )
3		sbcimg 3843	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))))
4	3	biimpd 229	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))))
5	1, 2, 4	e12 44722	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))   )
6		sbcimg 3843	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))
7	1, 6	e1a 44625	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   )
8		imbi2 348	. . . . . 6 ⊢ (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))
9	8	biimpcd 249	. . . . 5 ⊢ (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) → (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))
10	5, 7, 9	e21 44728	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   )
11	10	in2 44603	. . 3 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))   )
12		idn2 44611	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   )
13		biimpr 220	. . . . . . 7 ⊢ (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒) → [𝐴 / 𝑥](𝜓 → 𝜒)))
14	13	imim2d 57	. . . . . 6 ⊢ (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))))
15	7, 12, 14	e12 44722	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))   )
16	1, 3	e1a 44625	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)))   )
17		biimpr 220	. . . . . 6 ⊢ (([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))) → (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))))
18	17	com12 32	. . . . 5 ⊢ (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) → (([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))))
19	15, 16, 18	e21 44728	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   ▶   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   )
20	19	in2 44603	. . 3 ⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)))   )
21		impbi 208	. . 3 ⊢ (([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))) → ((([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))) → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))))
22	11, 20, 21	e11 44686	. 2 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))   )
23	22	in1 44569	1 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2106  [wsbc 3791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-sbc 3792  df-vd1 44568  df-vd2 44576

This theorem is referenced by: (None)