Theorem sbc3orgVD 16675

Description: Virtual deduction proof of sbc3org 5827. 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,?: e1_ 16518	|- . 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 16585	|- . A e. B   ⊢   [A / x](((ph \/ ps) \/ ch) <-> (ph \/ ps \/ ch)) .
4:1,33,?: e11 16578	|- . A e. B   ⊢   ([A / x]((ph \/ ps) \/ ch) <-> [A / x](ph \/ ps \/ ch)) .
5:2,4,?: e11 16578	|- . A e. B   ⊢   ([A / x](ph \/ ps \/ ch) <-> ([A / x](ph \/ ps) \/ [A / x]ch)) .
6:1,?: e1_ 16518	|- . A e. B   ⊢   ([A / x](ph \/ ps) <-> ([A / x]ph \/ [A / x]ps)) .
7:6,?: e1_ 16518	|- . A e. B   ⊢   (([A / x](ph \/ ps) \/ [A / x]ch) <-> (([A / x]ph \/ [A / x]ps) \/ [A / x]ch)) .
8:5,7,?: e11 16578	|- . 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 16585	|- . 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)))

Assertion

Ref	Expression
sbc3orgVD	|- (A e. B -> ([A / x](ph \/ ps \/ ch) <-> ([A / x]ph \/ [A / x]ps \/ [A / x]ch)))

Proof of Theorem sbc3orgVD

Step	Hyp	Ref	Expression
1		idn1 16484	. . . . . 6 |- . A e. B   ⊢   A e. B .
2		sbcorg 2498	. . . . . 6 |- (A e. B -> ([A / x]((ph \/ ps) \/ ch) <-> ([A / x](ph \/ ps) \/ [A / x]ch)))
3	1, 2	e1_ 16518	. . . . 5 |- . A e. B   ⊢   ([A / x]((ph \/ ps) \/ ch) <-> ([A / x](ph \/ ps) \/ [A / x]ch)) .
4		df-3or 859	. . . . . . . . 9 |- ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))
5	4	bicomi 189	. . . . . . . 8 |- (((ph \/ ps) \/ ch) <-> (ph \/ ps \/ ch))
6	5	ax-gen 1305	. . . . . . 7 |- A.x(((ph \/ ps) \/ ch) <-> (ph \/ ps \/ ch))
7		a4sbc 2457	. . . . . . 7 |- (A e. B -> (A.x(((ph \/ ps) \/ ch) <-> (ph \/ ps \/ ch)) -> [A / x](((ph \/ ps) \/ ch) <-> (ph \/ ps \/ ch))))
8	1, 6, 7	e10 16585	. . . . . 6 |- . A e. B   ⊢   [A / x](((ph \/ ps) \/ ch) <-> (ph \/ ps \/ ch)) .
9		sbcbidig 2499	. . . . . . 7 |- (A e. B -> ([A / x](((ph \/ ps) \/ ch) <-> (ph \/ ps \/ ch)) <-> ([A / x]((ph \/ ps) \/ ch) <-> [A / x](ph \/ ps \/ ch))))
10	9	biimpd 170	. . . . . 6 |- (A e. B -> ([A / x](((ph \/ ps) \/ ch) <-> (ph \/ ps \/ ch)) -> ([A / x]((ph \/ ps) \/ ch) <-> [A / x](ph \/ ps \/ ch))))
11	1, 8, 10	e11 16578	. . . . 5 |- . A e. B   ⊢   ([A / x]((ph \/ ps) \/ ch) <-> [A / x](ph \/ ps \/ ch)) .
12		bitr3 1283	. . . . . 6 |- (([A / x]((ph \/ ps) \/ ch) <-> [A / x](ph \/ ps \/ ch)) -> (([A / x]((ph \/ ps) \/ ch) <-> ([A / x](ph \/ ps) \/ [A / x]ch)) -> ([A / x](ph \/ ps \/ ch) <-> ([A / x](ph \/ ps) \/ [A / x]ch))))
13	12	com12 14	. . . . 5 |- (([A / x]((ph \/ ps) \/ ch) <-> ([A / x](ph \/ ps) \/ [A / x]ch)) -> (([A / x]((ph \/ ps) \/ ch) <-> [A / x](ph \/ ps \/ ch)) -> ([A / x](ph \/ ps \/ ch) <-> ([A / x](ph \/ ps) \/ [A / x]ch))))
14	3, 11, 13	e11 16578	. . . 4 |- . A e. B   ⊢   ([A / x](ph \/ ps \/ ch) <-> ([A / x](ph \/ ps) \/ [A / x]ch)) .
15		sbcorg 2498	. . . . . 6 |- (A e. B -> ([A / x](ph \/ ps) <-> ([A / x]ph \/ [A / x]ps)))
16	1, 15	e1_ 16518	. . . . 5 |- . A e. B   ⊢   ([A / x](ph \/ ps) <-> ([A / x]ph \/ [A / x]ps)) .
17		orbi1 682	. . . . 5 |- (([A / x](ph \/ ps) <-> ([A / x]ph \/ [A / x]ps)) -> (([A / x](ph \/ ps) \/ [A / x]ch) <-> (([A / x]ph \/ [A / x]ps) \/ [A / x]ch)))
18	16, 17	e1_ 16518	. . . 4 |- . A e. B   ⊢   (([A / x](ph \/ ps) \/ [A / x]ch) <-> (([A / x]ph \/ [A / x]ps) \/ [A / x]ch)) .
19		bibi1 687	. . . . 5 |- (([A / x](ph \/ ps \/ ch) <-> ([A / x](ph \/ ps) \/ [A / x]ch)) -> (([A / x](ph \/ ps \/ ch) <-> (([A / x]ph \/ [A / x]ps) \/ [A / x]ch)) <-> (([A / x](ph \/ ps) \/ [A / x]ch) <-> (([A / x]ph \/ [A / x]ps) \/ [A / x]ch))))
20	19	biimprd 171	. . . 4 |- (([A / x](ph \/ ps \/ ch) <-> ([A / x](ph \/ ps) \/ [A / x]ch)) -> ((([A / x](ph \/ ps) \/ [A / x]ch) <-> (([A / x]ph \/ [A / x]ps) \/ [A / x]ch)) -> ([A / x](ph \/ ps \/ ch) <-> (([A / x]ph \/ [A / x]ps) \/ [A / x]ch))))
21	14, 18, 20	e11 16578	. . 3 |- . A e. B   ⊢   ([A / x](ph \/ ps \/ ch) <-> (([A / x]ph \/ [A / x]ps) \/ [A / x]ch)) .
22		df-3or 859	. . . 4 |- (([A / x]ph \/ [A / x]ps \/ [A / x]ch) <-> (([A / x]ph \/ [A / x]ps) \/ [A / x]ch))
23	22	bicomi 189	. . 3 |- ((([A / x]ph \/ [A / x]ps) \/ [A / x]ch) <-> ([A / x]ph \/ [A / x]ps \/ [A / x]ch))
24		bibi1 687	. . . 4 |- (([A / x](ph \/ ps \/ ch) <-> (([A / x]ph \/ [A / x]ps) \/ [A / x]ch)) -> (([A / x](ph \/ ps \/ ch) <-> ([A / x]ph \/ [A / x]ps \/ [A / x]ch)) <-> ((([A / x]ph \/ [A / x]ps) \/ [A / x]ch) <-> ([A / x]ph \/ [A / x]ps \/ [A / x]ch))))
25	24	biimprd 171	. . 3 |- (([A / x](ph \/ ps \/ ch) <-> (([A / x]ph \/ [A / x]ps) \/ [A / x]ch)) -> (((([A / x]ph \/ [A / x]ps) \/ [A / x]ch) <-> ([A / x]ph \/ [A / x]ps \/ [A / x]ch)) -> ([A / x](ph \/ ps \/ ch) <-> ([A / x]ph \/ [A / x]ps \/ [A / x]ch))))
26	21, 23, 25	e10 16585	. 2 |- . A e. B   ⊢   ([A / x](ph \/ ps \/ ch) <-> ([A / x]ph \/ [A / x]ps \/ [A / x]ch)) .
27	26	in1 16481	1 |- (A e. B -> ([A / x](ph \/ ps \/ ch) <-> ([A / x]ph \/ [A / x]ps \/ [A / x]ch)))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   \/ w3o 857  A.wal 1296   e. wcel 1300  [wsbc 1534

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-sbc 2454  df-vd1 16480

Copyright terms: Public domain