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 44495
Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg 3843. sbcim2g 44495 is sbcim2gVD 44832 without virtual deductions and was automatically derived from sbcim2gVD 44832 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 3843 . . . 4 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))))
21biimpd 229 . . 3 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))))
3 sbcimg 3843 . . 3 (𝐴𝑉 → ([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)))
4 imbi2 348 . . . 4 (([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
54biimpcd 249 . . 3 (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒)) → (([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
62, 3, 5syl6ci 71 . 2 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
7 idd 24 . . . 4 (𝐴𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
8 biimpr 220 . . . 4 (([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒) → [𝐴 / 𝑥](𝜓𝜒)))
93, 7, 8ee13 44461 . . 3 (𝐴𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))))
109, 1sylibrd 259 . 2 (𝐴𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓𝜒))))
116, 10impbid 212 1 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wcel 2104  [wsbc 3791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003  ax-8 2106  ax-9 2114  ax-10 2137  ax-12 2173  ax-ext 2704
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1538  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2711  df-cleq 2725  df-clel 2812  df-sbc 3792
This theorem is referenced by:  trsbc  44497  trsbcVD  44834
  Copyright terms: Public domain W3C validator