# 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

### Proof

Step Hyp Ref Expression
1 idn1 ${⊢}\left({A}\in {B}{\to }{A}\in {B}\right)$
2 sbcor
3 2 a1i
4 1 3 e1a
5 df-3or ${⊢}\left({\phi }\vee {\psi }\vee {\chi }\right)↔\left(\left({\phi }\vee {\psi }\right)\vee {\chi }\right)$
6 5 bicomi ${⊢}\left(\left({\phi }\vee {\psi }\right)\vee {\chi }\right)↔\left({\phi }\vee {\psi }\vee {\chi }\right)$
7 6 ax-gen ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left(\left({\phi }\vee {\psi }\right)\vee {\chi }\right)↔\left({\phi }\vee {\psi }\vee {\chi }\right)\right)$
8 spsbc
9 1 7 8 e10
10 sbcbig
11 10 biimpd
12 1 9 11 e11
13 bitr3
14 13 com12
15 4 12 14 e11
16 sbcor
17 16 a1i
18 1 17 e1a
19 orbi1
20 18 19 e1a
21 bibi1
22 21 biimprd
23 15 20 22 e11
24 df-3or
25 24 bicomi
26 bibi1
27 26 biimprd
28 23 25 27 e10
29 28 in1