Theorem sbcim2gVD 40625

Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg 3725. 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 40288 is sbcim2gVD 40625 without virtual deductions and was automatically derived from sbcim2gVD 40625.

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 40324	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2		idn2 40363	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   ▶   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   )
3		sbcimg 3725	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))))
4	3	biimpd 221	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))))
5	1, 2, 4	e12 40474	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))   )
6		sbcimg 3725	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))
7	1, 6	e1a 40377	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   )
8		imbi2 341	. . . . . 6 ⊢ (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))
9	8	biimpcd 241	. . . . 5 ⊢ (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) → (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))
10	5, 7, 9	e21 40480	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   )
11	10	in2 40355	. . 3 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))   )
12		idn2 40363	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   )
13		biimpr 212	. . . . . . 7 ⊢ (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒) → [𝐴 / 𝑥](𝜓 → 𝜒)))
14	13	imim2d 57	. . . . . 6 ⊢ (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))))
15	7, 12, 14	e12 40474	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))   )
16	1, 3	e1a 40377	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)))   )
17		biimpr 212	. . . . . 6 ⊢ (([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))) → (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))))
18	17	com12 32	. . . . 5 ⊢ (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) → (([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))))
19	15, 16, 18	e21 40480	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   ▶   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   )
20	19	in2 40355	. . 3 ⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)))   )
21		impbi 200	. . 3 ⊢ (([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))) → ((([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))) → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))))
22	11, 20, 21	e11 40438	. 2 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))   )
23	22	in1 40321	1 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))

Syntax hints:   → wi 4   ↔ wb 198   ∈ wcel 2050  [wsbc 3682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-12 2106  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-sbc 3683  df-vd1 40320  df-vd2 40328

This theorem is referenced by: (None)