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

Theorem sbc3orgVD 41505
Description: Virtual deduction proof of the analogue of sbcor 3807 with three disjuncts. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
1:: (   𝐴𝐵   ▶   𝐴𝐵   )
2:1,?: e1a 41281 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]((𝜑 𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) [𝐴 / 𝑥]𝜒))   )
3:: (((𝜑𝜓) ∨ 𝜒) ↔ (𝜑 𝜓𝜒))
32:3: 𝑥(((𝜑𝜓) ∨ 𝜒) ↔ (𝜑𝜓𝜒))
33:1,32,?: e10 41348 (   𝐴𝐵   ▶   [𝐴 / 𝑥](((𝜑 𝜓) ∨ 𝜒) ↔ (𝜑𝜓𝜒))   )
4:1,33,?: e11 41342 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]((𝜑 𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑𝜓𝜒))   )
5:2,4,?: e11 41342 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 𝜓𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
6:1,?: e1a 41281 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))   )
7:6,?: e1a 41281 (   𝐴𝐵   ▶   (([𝐴 / 𝑥](𝜑 𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) [𝐴 / 𝑥]𝜒))   )
8:5,7,?: e11 41342 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 𝜓𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) [𝐴 / 𝑥]𝜒))   )
9:?: ((([𝐴 / 𝑥]𝜑 [𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑 [𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))
10:8,9,?: e10 41348 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑 𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓 [𝐴 / 𝑥]𝜒))   )
qed:10: (𝐴𝐵 → ([𝐴 / 𝑥](𝜑 𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓 [𝐴 / 𝑥]𝜒)))
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
sbc3orgVD (𝐴𝐵 → ([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)))

Proof of Theorem sbc3orgVD
StepHypRef Expression
1 idn1 41228 . . . . . 6 (   𝐴𝐵   ▶   𝐴𝐵   )
2 sbcor 3807 . . . . . . 7 ([𝐴 / 𝑥]((𝜑𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒))
32a1i 11 . . . . . 6 (𝐴𝐵 → ([𝐴 / 𝑥]((𝜑𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒)))
41, 3e1a 41281 . . . . 5 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]((𝜑𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
5 df-3or 1085 . . . . . . . . 9 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
65bicomi 227 . . . . . . . 8 (((𝜑𝜓) ∨ 𝜒) ↔ (𝜑𝜓𝜒))
76ax-gen 1797 . . . . . . 7 𝑥(((𝜑𝜓) ∨ 𝜒) ↔ (𝜑𝜓𝜒))
8 spsbc 3771 . . . . . . 7 (𝐴𝐵 → (∀𝑥(((𝜑𝜓) ∨ 𝜒) ↔ (𝜑𝜓𝜒)) → [𝐴 / 𝑥](((𝜑𝜓) ∨ 𝜒) ↔ (𝜑𝜓𝜒))))
91, 7, 8e10 41348 . . . . . 6 (   𝐴𝐵   ▶   [𝐴 / 𝑥](((𝜑𝜓) ∨ 𝜒) ↔ (𝜑𝜓𝜒))   )
10 sbcbig 3808 . . . . . . 7 (𝐴𝐵 → ([𝐴 / 𝑥](((𝜑𝜓) ∨ 𝜒) ↔ (𝜑𝜓𝜒)) ↔ ([𝐴 / 𝑥]((𝜑𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑𝜓𝜒))))
1110biimpd 232 . . . . . 6 (𝐴𝐵 → ([𝐴 / 𝑥](((𝜑𝜓) ∨ 𝜒) ↔ (𝜑𝜓𝜒)) → ([𝐴 / 𝑥]((𝜑𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑𝜓𝜒))))
121, 9, 11e11 41342 . . . . 5 (   𝐴𝐵   ▶   ([𝐴 / 𝑥]((𝜑𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑𝜓𝜒))   )
13 bitr3 356 . . . . . 6 (([𝐴 / 𝑥]((𝜑𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑𝜓𝜒)) → (([𝐴 / 𝑥]((𝜑𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒))))
1413com12 32 . . . . 5 (([𝐴 / 𝑥]((𝜑𝜓) ∨ 𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥]((𝜑𝜓) ∨ 𝜒) ↔ [𝐴 / 𝑥](𝜑𝜓𝜒)) → ([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒))))
154, 12, 14e11 41342 . . . 4 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
16 sbcor 3807 . . . . . . 7 ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
1716a1i 11 . . . . . 6 (𝐴𝐵 → ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)))
181, 17e1a 41281 . . . . 5 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))   )
19 orbi1 915 . . . . 5 (([𝐴 / 𝑥](𝜑𝜓) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓)) → (([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)))
2018, 19e1a 41281 . . . 4 (   𝐴𝐵   ▶   (([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
21 bibi1 355 . . . . 5 (([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)) ↔ (([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))))
2221biimprd 251 . . . 4 (([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ ([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒)) → ((([𝐴 / 𝑥](𝜑𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))))
2315, 20, 22e11 41342 . . 3 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))   )
24 df-3or 1085 . . . 4 (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒))
2524bicomi 227 . . 3 ((([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))
26 bibi1 355 . . . 4 (([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)) → (([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) ↔ ((([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
2726biimprd 251 . . 3 (([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ (([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒)) → (((([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓) ∨ [𝐴 / 𝑥]𝜒) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)) → ([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))))
2823, 25, 27e10 41348 . 2 (   𝐴𝐵   ▶   ([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒))   )
2928in1 41225 1 (𝐴𝐵 → ([𝐴 / 𝑥](𝜑𝜓𝜒) ↔ ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓[𝐴 / 𝑥]𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wo 844  w3o 1083  wal 1536  wcel 2115  [wsbc 3758
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-sbc 3759  df-vd1 41224
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator