Metamath Proof Explorer


Theorem poclOLD

Description: Obsolete version of pocl as of 3-Oct-2024. (Contributed by NM, 27-Mar-1997) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion poclOLD R Po A B A C A D A ¬ B R B B R C C R D B R D

Proof

Step Hyp Ref Expression
1 id x = B x = B
2 1 1 breq12d x = B x R x B R B
3 2 notbid x = B ¬ x R x ¬ B R B
4 breq1 x = B x R y B R y
5 4 anbi1d x = B x R y y R z B R y y R z
6 breq1 x = B x R z B R z
7 5 6 imbi12d x = B x R y y R z x R z B R y y R z B R z
8 3 7 anbi12d x = B ¬ x R x x R y y R z x R z ¬ B R B B R y y R z B R z
9 8 imbi2d x = B R Po A ¬ x R x x R y y R z x R z R Po A ¬ B R B B R y y R z B R z
10 breq2 y = C B R y B R C
11 breq1 y = C y R z C R z
12 10 11 anbi12d y = C B R y y R z B R C C R z
13 12 imbi1d y = C B R y y R z B R z B R C C R z B R z
14 13 anbi2d y = C ¬ B R B B R y y R z B R z ¬ B R B B R C C R z B R z
15 14 imbi2d y = C R Po A ¬ B R B B R y y R z B R z R Po A ¬ B R B B R C C R z B R z
16 breq2 z = D C R z C R D
17 16 anbi2d z = D B R C C R z B R C C R D
18 breq2 z = D B R z B R D
19 17 18 imbi12d z = D B R C C R z B R z B R C C R D B R D
20 19 anbi2d z = D ¬ B R B B R C C R z B R z ¬ B R B B R C C R D B R D
21 20 imbi2d z = D R Po A ¬ B R B B R C C R z B R z R Po A ¬ B R B B R C C R D B R D
22 df-po R Po A x A y A z A ¬ x R x x R y y R z x R z
23 r3al x A y A z A ¬ x R x x R y y R z x R z x y z x A y A z A ¬ x R x x R y y R z x R z
24 22 23 sylbb R Po A x y z x A y A z A ¬ x R x x R y y R z x R z
25 24 19.21bbi R Po A z x A y A z A ¬ x R x x R y y R z x R z
26 25 19.21bi R Po A x A y A z A ¬ x R x x R y y R z x R z
27 26 com12 x A y A z A R Po A ¬ x R x x R y y R z x R z
28 9 15 21 27 vtocl3ga B A C A D A R Po A ¬ B R B B R C C R D B R D
29 28 com12 R Po A B A C A D A ¬ B R B B R C C R D B R D