Metamath Proof Explorer

Theorem sbc3orgVD

Description: Virtual deduction proof of the analogue of sbcor 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:: |- (. A e. B ->. A e. B ).
2:1,?: e1a |- (. A e. B ->. ( [. A / x ]. ( ( ph \/ ps ) \/ ch ) <-> ( [. A / x ]. ( ph \/ ps ) \/ [. A / x ]. ch ) ) ).
3:: |- ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ps \/ ch ) )
32:3: |- A. x ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ps \/ ch ) )
33:1,32,?: e10 |- (. A e. B ->. [. A / x ]. ( ( ( ph \/ ps ) \/ ch ) <-> ( ph \/ ps \/ ch ) ) ).
4:1,33,?: e11 |- (. A e. B ->. ( [. A / x ]. ( ( ph \/ ps ) \/ ch ) <-> [. A / x ]. ( ph \/ ps \/ ch ) ) ).
5:2,4,?: e11 |- (. A e. B ->. ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( [. A / x ]. ( ph \/ ps ) \/ [. A / x ]. ch ) ) ).
6:1,?: e1a |- (. A e. B ->. ( [. A / x ]. ( ph \/ ps ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps ) ) ).
7:6,?: e1a |- (. A e. B ->. ( ( [. A / x ]. ( ph \/ ps ) \/ [. A / x ]. ch ) <-> ( ( [. A / x ]. ph \/ [. A / x ]. ps ) \/ [. A / x ]. ch ) ) ).
8:5,7,?: e11 |- (. A e. B ->. ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( ( [. A / x ]. ph \/ [. A / x ]. ps ) \/ [. A / x ]. ch ) ) ).
9:?: |- ( ( ( [. A / x ]. ph \/ [. A / x ]. ps ) \/ [. A / x ]. ch ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps \/ [. A / x ]. ch ) )
10:8,9,?: e10 |- (. A e. B ->. ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps \/ [. A / x ]. ch ) ) ).
qed:10: |- ( A e. B -> ( [. A / x ]. ( ph \/ ps \/ ch ) <-> ( [. A / x ]. ph \/ [. A / x ]. ps \/ [. A / x ]. ch ) ) )
(Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbc3orgVD ⊢A∈B→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ

Proof

Step Hyp Ref Expression
1 idn1 ⊢A∈B→A∈B
2 sbcor ⊢[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨[˙A/x]˙χ
3 2 a1i ⊢A∈B→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨[˙A/x]˙χ
4 1 3 e1a ⊢A∈B→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨[˙A/x]˙χ
5 df-3or ⊢φ∨ψ∨χ↔φ∨ψ∨χ
6 5 bicomi ⊢φ∨ψ∨χ↔φ∨ψ∨χ
7 6 ax-gen ⊢∀xφ∨ψ∨χ↔φ∨ψ∨χ
8 spsbc ⊢A∈B→∀xφ∨ψ∨χ↔φ∨ψ∨χ→[˙A/x]˙φ∨ψ∨χ↔φ∨ψ∨χ
9 1 7 8 e10 ⊢A∈B→[˙A/x]˙φ∨ψ∨χ↔φ∨ψ∨χ
10 sbcbig ⊢A∈B→[˙A/x]˙φ∨ψ∨χ↔φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨χ
11 10 biimpd ⊢A∈B→[˙A/x]˙φ∨ψ∨χ↔φ∨ψ∨χ→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨χ
12 1 9 11 e11 ⊢A∈B→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨χ
13 bitr3 ⊢[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨χ→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨[˙A/x]˙χ→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨[˙A/x]˙χ
14 13 com12 ⊢[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨[˙A/x]˙χ→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨χ→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨[˙A/x]˙χ
15 4 12 14 e11 ⊢A∈B→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨[˙A/x]˙χ
16 sbcor ⊢[˙A/x]˙φ∨ψ↔[˙A/x]˙φ∨[˙A/x]˙ψ
17 16 a1i ⊢A∈B→[˙A/x]˙φ∨ψ↔[˙A/x]˙φ∨[˙A/x]˙ψ
18 1 17 e1a ⊢A∈B→[˙A/x]˙φ∨ψ↔[˙A/x]˙φ∨[˙A/x]˙ψ
19 orbi1 ⊢[˙A/x]˙φ∨ψ↔[˙A/x]˙φ∨[˙A/x]˙ψ→[˙A/x]˙φ∨ψ∨[˙A/x]˙χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ
20 18 19 e1a ⊢A∈B→[˙A/x]˙φ∨ψ∨[˙A/x]˙χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ
21 bibi1 ⊢[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨[˙A/x]˙χ→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ↔[˙A/x]˙φ∨ψ∨[˙A/x]˙χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ
22 21 biimprd ⊢[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨ψ∨[˙A/x]˙χ→[˙A/x]˙φ∨ψ∨[˙A/x]˙χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ
23 15 20 22 e11 ⊢A∈B→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ
24 df-3or ⊢[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ
25 24 bicomi ⊢[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ
26 bibi1 ⊢[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ
27 26 biimprd ⊢[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ→[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ
28 23 25 27 e10 ⊢A∈B→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ
29 28 in1 ⊢A∈B→[˙A/x]˙φ∨ψ∨χ↔[˙A/x]˙φ∨[˙A/x]˙ψ∨[˙A/x]˙χ