Theorem sbcim2gVD 39603

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

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 39286	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ▶   𝐴 ∈ 𝐵   )
2		idn2 39334	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   ▶   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   )
3		sbcimg 3673	. . . . . . 7 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))))
4	3	biimpd 220	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))))
5	1, 2, 4	e12 39446	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))   )
6		sbcimg 3673	. . . . . 6 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))
7	1, 6	e1a 39348	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   )
8		imbi2 339	. . . . . 6 ⊢ (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))
9	8	biimpcd 240	. . . . 5 ⊢ (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) → (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))
10	5, 7, 9	e21 39452	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   )
11	10	in2 39326	. . 3 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))   )
12		idn2 39334	. . . . . 6 ⊢ (   𝐴 ∈ 𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   )
13		biimpr 211	. . . . . . 7 ⊢ (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒) → [𝐴 / 𝑥](𝜓 → 𝜒)))
14	13	imim2d 57	. . . . . 6 ⊢ (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))))
15	7, 12, 14	e12 39446	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))   )
16	1, 3	e1a 39348	. . . . 5 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)))   )
17		biimpr 211	. . . . . 6 ⊢ (([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))) → (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))))
18	17	com12 32	. . . . 5 ⊢ (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) → (([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))))
19	15, 16, 18	e21 39452	. . . 4 ⊢ (   𝐴 ∈ 𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))   ▶   [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))   )
20	19	in2 39326	. . 3 ⊢ (   𝐴 ∈ 𝐵   ▶   (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)))   )
21		impbi 199	. . 3 ⊢ (([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))) → ((([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))) → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))))
22	11, 20, 21	e11 39409	. 2 ⊢ (   𝐴 ∈ 𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))   )
23	22	in1 39283	1 ⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))

Syntax hints:   → wi 4   ↔ wb 197   ∈ wcel 2156  [wsbc 3631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-12 2214  ax-13 2420  ax-ext 2782

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2791  df-cleq 2797  df-clel 2800  df-v 3391  df-sbc 3632  df-vd1 39282  df-vd2 39290

This theorem is referenced by: (None)