Theorem sbcim2g 39242

Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg 3610. sbcim2g 39242 is sbcim2gVD 39602 without virtual deductions and was automatically derived from sbcim2gVD 39602 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Proof of Theorem sbcim2g

Step	Hyp	Ref	Expression
1		sbcimg 3610	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))))
2	1	biimpd 219	. . 3 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))))
3		sbcimg 3610	. . 3 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)))
4		imbi2 337	. . . 4 ⊢ (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))
5	4	biimpcd 239	. . 3 ⊢ (([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒)) → (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))
6	2, 3, 5	syl6ci 71	. 2 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))
7		idd 24	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))
8		biimpr 210	. . . 4 ⊢ (([𝐴 / 𝑥](𝜓 → 𝜒) ↔ ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒) → [𝐴 / 𝑥](𝜓 → 𝜒)))
9	3, 7, 8	ee13 39204	. . 3 ⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → [𝐴 / 𝑥](𝜓 → 𝜒))))
10	9, 1	sylibrd 249	. 2 ⊢ (𝐴 ∈ 𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒))))
11	6, 10	impbid 202	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓 → 𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓 → [𝐴 / 𝑥]𝜒))))

Syntax hints:   → wi 4   ↔ wb 196   ∈ wcel 2131  [wsbc 3568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-v 3334  df-sbc 3569

This theorem is referenced by:  trsbc  39244  trsbcVD  39604