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 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
StepHypRef Expression
1 sbcimg 3610 . . . 4 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))))
21biimpd 219 . . 3 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))))
3 sbcimg 3610 . . 3 (𝐴𝑉 → ([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)))
4 imbi2 337 . . . 4 (([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
54biimpcd 239 . . 3 (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒)) → (([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
62, 3, 5syl6ci 71 . 2 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
7 idd 24 . . . 4 (𝐴𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
8 biimpr 210 . . . 4 (([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒) → [𝐴 / 𝑥](𝜓𝜒)))
93, 7, 8ee13 39204 . . 3 (𝐴𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))))
109, 1sylibrd 249 . 2 (𝐴𝑉 → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓𝜒))))
116, 10impbid 202 1 (𝐴𝑉 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator