Step | Hyp | Ref
| Expression |
1 | | elxp7 7957 |
. . . . . 6
ā¢ (š¤ ā (šµ Ć š¶) ā (š¤ ā (V Ć V) ā§ ((1st
āš¤) ā šµ ā§ (2nd
āš¤) ā š¶))) |
2 | 1 | anbi1i 625 |
. . . . 5
ā¢ ((š¤ ā (šµ Ć š¶) ā§ (2nd āš¤) ā š“) ā ((š¤ ā (V Ć V) ā§ ((1st
āš¤) ā šµ ā§ (2nd
āš¤) ā š¶)) ā§ (2nd
āš¤) ā š“)) |
3 | | ssel 3938 |
. . . . . . . 8
ā¢ (š“ ā š¶ ā ((2nd āš¤) ā š“ ā (2nd āš¤) ā š¶)) |
4 | 3 | pm4.71rd 564 |
. . . . . . 7
ā¢ (š“ ā š¶ ā ((2nd āš¤) ā š“ ā ((2nd āš¤) ā š¶ ā§ (2nd āš¤) ā š“))) |
5 | 4 | anbi2d 630 |
. . . . . 6
ā¢ (š“ ā š¶ ā (((š¤ ā (V Ć V) ā§ (1st
āš¤) ā šµ) ā§ (2nd
āš¤) ā š“) ā ((š¤ ā (V Ć V) ā§ (1st
āš¤) ā šµ) ā§ ((2nd
āš¤) ā š¶ ā§ (2nd
āš¤) ā š“)))) |
6 | | anass 470 |
. . . . . . . 8
ā¢ ((((š¤ ā (V Ć V) ā§
(1st āš¤)
ā šµ) ā§
(2nd āš¤)
ā š¶) ā§
(2nd āš¤)
ā š“) ā ((š¤ ā (V Ć V) ā§
(1st āš¤)
ā šµ) ā§
((2nd āš¤)
ā š¶ ā§
(2nd āš¤)
ā š“))) |
7 | 6 | bicomi 223 |
. . . . . . 7
ā¢ (((š¤ ā (V Ć V) ā§
(1st āš¤)
ā šµ) ā§
((2nd āš¤)
ā š¶ ā§
(2nd āš¤)
ā š“)) ā (((š¤ ā (V Ć V) ā§
(1st āš¤)
ā šµ) ā§
(2nd āš¤)
ā š¶) ā§
(2nd āš¤)
ā š“)) |
8 | 7 | a1i 11 |
. . . . . 6
ā¢ (š“ ā š¶ ā (((š¤ ā (V Ć V) ā§ (1st
āš¤) ā šµ) ā§ ((2nd
āš¤) ā š¶ ā§ (2nd
āš¤) ā š“)) ā (((š¤ ā (V Ć V) ā§ (1st
āš¤) ā šµ) ā§ (2nd
āš¤) ā š¶) ā§ (2nd
āš¤) ā š“))) |
9 | | anass 470 |
. . . . . . . 8
ā¢ (((š¤ ā (V Ć V) ā§
(1st āš¤)
ā šµ) ā§
(2nd āš¤)
ā š¶) ā (š¤ ā (V Ć V) ā§
((1st āš¤)
ā šµ ā§
(2nd āš¤)
ā š¶))) |
10 | 9 | anbi1i 625 |
. . . . . . 7
ā¢ ((((š¤ ā (V Ć V) ā§
(1st āš¤)
ā šµ) ā§
(2nd āš¤)
ā š¶) ā§
(2nd āš¤)
ā š“) ā ((š¤ ā (V Ć V) ā§
((1st āš¤)
ā šµ ā§
(2nd āš¤)
ā š¶)) ā§
(2nd āš¤)
ā š“)) |
11 | 10 | a1i 11 |
. . . . . 6
ā¢ (š“ ā š¶ ā ((((š¤ ā (V Ć V) ā§ (1st
āš¤) ā šµ) ā§ (2nd
āš¤) ā š¶) ā§ (2nd
āš¤) ā š“) ā ((š¤ ā (V Ć V) ā§ ((1st
āš¤) ā šµ ā§ (2nd
āš¤) ā š¶)) ā§ (2nd
āš¤) ā š“))) |
12 | 5, 8, 11 | 3bitrd 305 |
. . . . 5
ā¢ (š“ ā š¶ ā (((š¤ ā (V Ć V) ā§ (1st
āš¤) ā šµ) ā§ (2nd
āš¤) ā š“) ā ((š¤ ā (V Ć V) ā§ ((1st
āš¤) ā šµ ā§ (2nd
āš¤) ā š¶)) ā§ (2nd
āš¤) ā š“))) |
13 | 2, 12 | bitr4id 290 |
. . . 4
ā¢ (š“ ā š¶ ā ((š¤ ā (šµ Ć š¶) ā§ (2nd āš¤) ā š“) ā ((š¤ ā (V Ć V) ā§ (1st
āš¤) ā šµ) ā§ (2nd
āš¤) ā š“))) |
14 | | ancom 462 |
. . . 4
ā¢ ((š¤ ā (šµ Ć š¶) ā§ (2nd āš¤) ā š“) ā ((2nd āš¤) ā š“ ā§ š¤ ā (šµ Ć š¶))) |
15 | | anass 470 |
. . . 4
ā¢ (((š¤ ā (V Ć V) ā§
(1st āš¤)
ā šµ) ā§
(2nd āš¤)
ā š“) ā (š¤ ā (V Ć V) ā§
((1st āš¤)
ā šµ ā§
(2nd āš¤)
ā š“))) |
16 | 13, 14, 15 | 3bitr3g 313 |
. . 3
ā¢ (š“ ā š¶ ā (((2nd āš¤) ā š“ ā§ š¤ ā (šµ Ć š¶)) ā (š¤ ā (V Ć V) ā§ ((1st
āš¤) ā šµ ā§ (2nd
āš¤) ā š“)))) |
17 | | cnvresima 6183 |
. . . . 5
ā¢ (ā”(2nd ā¾ (šµ Ć š¶)) ā š“) = ((ā”2nd ā š“) ā© (šµ Ć š¶)) |
18 | 17 | eleq2i 2826 |
. . . 4
ā¢ (š¤ ā (ā”(2nd ā¾ (šµ Ć š¶)) ā š“) ā š¤ ā ((ā”2nd ā š“) ā© (šµ Ć š¶))) |
19 | | elin 3927 |
. . . 4
ā¢ (š¤ ā ((ā”2nd ā š“) ā© (šµ Ć š¶)) ā (š¤ ā (ā”2nd ā š“) ā§ š¤ ā (šµ Ć š¶))) |
20 | | vex 3448 |
. . . . . 6
ā¢ š¤ ā V |
21 | | fo2nd 7943 |
. . . . . . 7
ā¢
2nd :VāontoāV |
22 | | fofn 6759 |
. . . . . . 7
ā¢
(2nd :VāontoāV ā 2nd Fn V) |
23 | | elpreima 7009 |
. . . . . . 7
ā¢
(2nd Fn V ā (š¤ ā (ā”2nd ā š“) ā (š¤ ā V ā§ (2nd āš¤) ā š“))) |
24 | 21, 22, 23 | mp2b 10 |
. . . . . 6
ā¢ (š¤ ā (ā”2nd ā š“) ā (š¤ ā V ā§ (2nd āš¤) ā š“)) |
25 | 20, 24 | mpbiran 708 |
. . . . 5
ā¢ (š¤ ā (ā”2nd ā š“) ā (2nd āš¤) ā š“) |
26 | 25 | anbi1i 625 |
. . . 4
ā¢ ((š¤ ā (ā”2nd ā š“) ā§ š¤ ā (šµ Ć š¶)) ā ((2nd āš¤) ā š“ ā§ š¤ ā (šµ Ć š¶))) |
27 | 18, 19, 26 | 3bitri 297 |
. . 3
ā¢ (š¤ ā (ā”(2nd ā¾ (šµ Ć š¶)) ā š“) ā ((2nd āš¤) ā š“ ā§ š¤ ā (šµ Ć š¶))) |
28 | | elxp7 7957 |
. . 3
ā¢ (š¤ ā (šµ Ć š“) ā (š¤ ā (V Ć V) ā§ ((1st
āš¤) ā šµ ā§ (2nd
āš¤) ā š“))) |
29 | 16, 27, 28 | 3bitr4g 314 |
. 2
ā¢ (š“ ā š¶ ā (š¤ ā (ā”(2nd ā¾ (šµ Ć š¶)) ā š“) ā š¤ ā (šµ Ć š“))) |
30 | 29 | eqrdv 2731 |
1
ā¢ (š“ ā š¶ ā (ā”(2nd ā¾ (šµ Ć š¶)) ā š“) = (šµ Ć š“)) |