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 AB[˙A/x]˙φψχ[˙A/x]˙φ[˙A/x]˙ψ[˙A/x]˙χ

Proof

Step Hyp Ref Expression
1 idn1 ABAB
2 sbcor [˙A/x]˙φψχ[˙A/x]˙φψ[˙A/x]˙χ
3 2 a1i AB[˙A/x]˙φψχ[˙A/x]˙φψ[˙A/x]˙χ
4 1 3 e1a AB[˙A/x]˙φψχ[˙A/x]˙φψ[˙A/x]˙χ
5 df-3or φψχφψχ
6 5 bicomi φψχφψχ
7 6 ax-gen xφψχφψχ
8 spsbc ABxφψχφψχ[˙A/x]˙φψχφψχ
9 1 7 8 e10 AB[˙A/x]˙φψχφψχ
10 sbcbig AB[˙A/x]˙φψχφψχ[˙A/x]˙φψχ[˙A/x]˙φψχ
11 10 biimpd AB[˙A/x]˙φψχφψχ[˙A/x]˙φψχ[˙A/x]˙φψχ
12 1 9 11 e11 AB[˙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 AB[˙A/x]˙φψχ[˙A/x]˙φψ[˙A/x]˙χ
16 sbcor [˙A/x]˙φψ[˙A/x]˙φ[˙A/x]˙ψ
17 16 a1i AB[˙A/x]˙φψ[˙A/x]˙φ[˙A/x]˙ψ
18 1 17 e1a AB[˙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 AB[˙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 AB[˙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 AB[˙A/x]˙φψχ[˙A/x]˙φ[˙A/x]˙ψ[˙A/x]˙χ
29 28 in1 AB[˙A/x]˙φψχ[˙A/x]˙φ[˙A/x]˙ψ[˙A/x]˙χ