Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sbcim2g Structured version   Visualization version   GIF version

Theorem sbcim2g 40734
Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg 3823. sbcim2g 40734 is sbcim2gVD 41071 without virtual deductions and was automatically derived from sbcim2gVD 41071 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
StepHypRef Expression
1 sbcimg 3823 . . . 4 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))))
21biimpd 230 . . 3 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))))
3 sbcimg 3823 . . 3 (𝐴𝑉 → ([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)))
4 imbi2 350 . . . 4 (([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
54biimpcd 250 . . 3 (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒)) → (([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
62, 3, 5syl6ci 71 . 2 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
7 idd 24 . . . 4 (𝐴𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
8 biimpr 221 . . . 4 (([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒) → [𝐴 / 𝑥](𝜓𝜒)))
93, 7, 8ee13 40700 . . 3 (𝐴𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))))
109, 1sylibrd 260 . 2 (𝐴𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓𝜒))))
116, 10impbid 213 1 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wcel 2106  [wsbc 3775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2167  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-sbc 3776
This theorem is referenced by:  trsbc  40736  trsbcVD  41073
  Copyright terms: Public domain W3C validator