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 ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 ∨ [ 𝐴 / 𝑥 ] 𝜓 ∨ [ 𝐴 / 𝑥 ] 𝜒 ) ) )