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

Theorem sbcim2gVD 43718
Description: Distribution of class substitution over a left-nested implication. Similar to sbcimg 3828. 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 43381 is sbcim2gVD 43718 without virtual deductions and was automatically derived from sbcim2gVD 43718.
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
StepHypRef Expression
1 idn1 43417 . . . . . 6 (   𝐴𝐵   ▶   𝐴𝐵   )
2 idn2 43456 . . . . . 6 (   𝐴𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓𝜒))   ▶   [𝐴 / 𝑥](𝜑 → (𝜓𝜒))   )
3 sbcimg 3828 . . . . . . 7 (𝐴𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))))
43biimpd 228 . . . . . 6 (𝐴𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))))
51, 2, 4e12 43567 . . . . 5 (   𝐴𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓𝜒))   ▶   ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))   )
6 sbcimg 3828 . . . . . 6 (𝐴𝐵 → ([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)))
71, 6e1a 43470 . . . . 5 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))   )
8 imbi2 348 . . . . . 6 (([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
98biimpcd 248 . . . . 5 (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒)) → (([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
105, 7, 9e21 43573 . . . 4 (   𝐴𝐵   ,   [𝐴 / 𝑥](𝜑 → (𝜓𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))   )
1110in2 43448 . . 3 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)))   )
12 idn2 43456 . . . . . 6 (   𝐴𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))   ▶   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))   )
13 biimpr 219 . . . . . . 7 (([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒) → [𝐴 / 𝑥](𝜓𝜒)))
1413imim2d 57 . . . . . 6 (([𝐴 / 𝑥](𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))))
157, 12, 14e12 43567 . . . . 5 (   𝐴𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))   ▶   ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))   )
161, 3e1a 43470 . . . . 5 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒)))   )
17 biimpr 219 . . . . . 6 (([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))) → (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓𝜒))))
1817com12 32 . . . . 5 (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒)) → (([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥](𝜓𝜒))) → [𝐴 / 𝑥](𝜑 → (𝜓𝜒))))
1915, 16, 18e21 43573 . . . 4 (   𝐴𝐵   ,   ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))   ▶   [𝐴 / 𝑥](𝜑 → (𝜓𝜒))   )
2019in2 43448 . . 3 (   𝐴𝐵   ▶   (([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓𝜒)))   )
21 impbi 207 . . 3 (([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) → ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))) → ((([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → [𝐴 / 𝑥](𝜑 → (𝜓𝜒))) → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)))))
2211, 20, 21e11 43531 . 2 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)))   )
2322in1 43414 1 (𝐴𝐵 → ([𝐴 / 𝑥](𝜑 → (𝜓𝜒)) ↔ ([𝐴 / 𝑥]𝜑 → ([𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2106  [wsbc 3777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sbc 3778  df-vd1 43413  df-vd2 43421
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator