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 (    𝐴𝐵    ▶    𝐴𝐵    )
2 sbcor ( [ 𝐴 / 𝑥 ] ( ( 𝜑𝜓 ) ∨ 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] ( 𝜑𝜓 ) ∨ [ 𝐴 / 𝑥 ] 𝜒 ) )
3 2 a1i ( 𝐴𝐵 → ( [ 𝐴 / 𝑥 ] ( ( 𝜑𝜓 ) ∨ 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] ( 𝜑𝜓 ) ∨ [ 𝐴 / 𝑥 ] 𝜒 ) ) )
4 1 3 e1a (    𝐴𝐵    ▶    ( [ 𝐴 / 𝑥 ] ( ( 𝜑𝜓 ) ∨ 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] ( 𝜑𝜓 ) ∨ [ 𝐴 / 𝑥 ] 𝜒 ) )    )
5 df-3or ( ( 𝜑𝜓𝜒 ) ↔ ( ( 𝜑𝜓 ) ∨ 𝜒 ) )
6 5 bicomi ( ( ( 𝜑𝜓 ) ∨ 𝜒 ) ↔ ( 𝜑𝜓𝜒 ) )
7 6 ax-gen 𝑥 ( ( ( 𝜑𝜓 ) ∨ 𝜒 ) ↔ ( 𝜑𝜓𝜒 ) )
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 ( 𝐴𝐵 → ( [ 𝐴 / 𝑥 ] ( 𝜑𝜓𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑[ 𝐴 / 𝑥 ] 𝜓[ 𝐴 / 𝑥 ] 𝜒 ) ) )