Step | Hyp | Ref
| Expression |
1 | | elxp7 7957 |
. . . . . 6
ā¢ (š¤ ā (šµ Ć š¶) ā (š¤ ā (V Ć V) ā§ ((1st
āš¤) ā šµ ā§ (2nd
āš¤) ā š¶))) |
2 | 1 | anbi2i 624 |
. . . . 5
ā¢
(((1st āš¤) ā š“ ā§ š¤ ā (šµ Ć š¶)) ā ((1st āš¤) ā š“ ā§ (š¤ ā (V Ć V) ā§ ((1st
āš¤) ā šµ ā§ (2nd
āš¤) ā š¶)))) |
3 | | anass 470 |
. . . . . . 7
ā¢
((((1st āš¤) ā š“ ā§ (1st āš¤) ā šµ) ā§ (š¤ ā (V Ć V) ā§ (2nd
āš¤) ā š¶)) ā ((1st
āš¤) ā š“ ā§ ((1st
āš¤) ā šµ ā§ (š¤ ā (V Ć V) ā§ (2nd
āš¤) ā š¶)))) |
4 | 3 | a1i 11 |
. . . . . 6
ā¢ (š“ ā šµ ā ((((1st āš¤) ā š“ ā§ (1st āš¤) ā šµ) ā§ (š¤ ā (V Ć V) ā§ (2nd
āš¤) ā š¶)) ā ((1st
āš¤) ā š“ ā§ ((1st
āš¤) ā šµ ā§ (š¤ ā (V Ć V) ā§ (2nd
āš¤) ā š¶))))) |
5 | | ssel 3938 |
. . . . . . . 8
ā¢ (š“ ā šµ ā ((1st āš¤) ā š“ ā (1st āš¤) ā šµ)) |
6 | 5 | pm4.71d 563 |
. . . . . . 7
ā¢ (š“ ā šµ ā ((1st āš¤) ā š“ ā ((1st āš¤) ā š“ ā§ (1st āš¤) ā šµ))) |
7 | 6 | anbi1d 631 |
. . . . . 6
ā¢ (š“ ā šµ ā (((1st āš¤) ā š“ ā§ (š¤ ā (V Ć V) ā§ (2nd
āš¤) ā š¶)) ā (((1st
āš¤) ā š“ ā§ (1st
āš¤) ā šµ) ā§ (š¤ ā (V Ć V) ā§ (2nd
āš¤) ā š¶)))) |
8 | | an12 644 |
. . . . . . . 8
ā¢ ((š¤ ā (V Ć V) ā§
((1st āš¤)
ā šµ ā§
(2nd āš¤)
ā š¶)) ā
((1st āš¤)
ā šµ ā§ (š¤ ā (V Ć V) ā§
(2nd āš¤)
ā š¶))) |
9 | 8 | anbi2i 624 |
. . . . . . 7
ā¢
(((1st āš¤) ā š“ ā§ (š¤ ā (V Ć V) ā§ ((1st
āš¤) ā šµ ā§ (2nd
āš¤) ā š¶))) ā ((1st
āš¤) ā š“ ā§ ((1st
āš¤) ā šµ ā§ (š¤ ā (V Ć V) ā§ (2nd
āš¤) ā š¶)))) |
10 | 9 | a1i 11 |
. . . . . 6
ā¢ (š“ ā šµ ā (((1st āš¤) ā š“ ā§ (š¤ ā (V Ć V) ā§ ((1st
āš¤) ā šµ ā§ (2nd
āš¤) ā š¶))) ā ((1st
āš¤) ā š“ ā§ ((1st
āš¤) ā šµ ā§ (š¤ ā (V Ć V) ā§ (2nd
āš¤) ā š¶))))) |
11 | 4, 7, 10 | 3bitr4d 311 |
. . . . 5
ā¢ (š“ ā šµ ā (((1st āš¤) ā š“ ā§ (š¤ ā (V Ć V) ā§ (2nd
āš¤) ā š¶)) ā ((1st
āš¤) ā š“ ā§ (š¤ ā (V Ć V) ā§ ((1st
āš¤) ā šµ ā§ (2nd
āš¤) ā š¶))))) |
12 | 2, 11 | bitr4id 290 |
. . . 4
ā¢ (š“ ā šµ ā (((1st āš¤) ā š“ ā§ š¤ ā (šµ Ć š¶)) ā ((1st āš¤) ā š“ ā§ (š¤ ā (V Ć V) ā§ (2nd
āš¤) ā š¶)))) |
13 | | an12 644 |
. . . 4
ā¢
(((1st āš¤) ā š“ ā§ (š¤ ā (V Ć V) ā§ (2nd
āš¤) ā š¶)) ā (š¤ ā (V Ć V) ā§ ((1st
āš¤) ā š“ ā§ (2nd
āš¤) ā š¶))) |
14 | 12, 13 | bitrdi 287 |
. . 3
ā¢ (š“ ā šµ ā (((1st āš¤) ā š“ ā§ š¤ ā (šµ Ć š¶)) ā (š¤ ā (V Ć V) ā§ ((1st
āš¤) ā š“ ā§ (2nd
āš¤) ā š¶)))) |
15 | | cnvresima 6183 |
. . . . 5
ā¢ (ā”(1st ā¾ (šµ Ć š¶)) ā š“) = ((ā”1st ā š“) ā© (šµ Ć š¶)) |
16 | 15 | eleq2i 2826 |
. . . 4
ā¢ (š¤ ā (ā”(1st ā¾ (šµ Ć š¶)) ā š“) ā š¤ ā ((ā”1st ā š“) ā© (šµ Ć š¶))) |
17 | | elin 3927 |
. . . 4
ā¢ (š¤ ā ((ā”1st ā š“) ā© (šµ Ć š¶)) ā (š¤ ā (ā”1st ā š“) ā§ š¤ ā (šµ Ć š¶))) |
18 | | vex 3448 |
. . . . . 6
ā¢ š¤ ā V |
19 | | fo1st 7942 |
. . . . . . 7
ā¢
1st :VāontoāV |
20 | | fofn 6759 |
. . . . . . 7
ā¢
(1st :VāontoāV ā 1st Fn V) |
21 | | elpreima 7009 |
. . . . . . 7
ā¢
(1st Fn V ā (š¤ ā (ā”1st ā š“) ā (š¤ ā V ā§ (1st āš¤) ā š“))) |
22 | 19, 20, 21 | mp2b 10 |
. . . . . 6
ā¢ (š¤ ā (ā”1st ā š“) ā (š¤ ā V ā§ (1st āš¤) ā š“)) |
23 | 18, 22 | mpbiran 708 |
. . . . 5
ā¢ (š¤ ā (ā”1st ā š“) ā (1st āš¤) ā š“) |
24 | 23 | anbi1i 625 |
. . . 4
ā¢ ((š¤ ā (ā”1st ā š“) ā§ š¤ ā (šµ Ć š¶)) ā ((1st āš¤) ā š“ ā§ š¤ ā (šµ Ć š¶))) |
25 | 16, 17, 24 | 3bitri 297 |
. . 3
ā¢ (š¤ ā (ā”(1st ā¾ (šµ Ć š¶)) ā š“) ā ((1st āš¤) ā š“ ā§ š¤ ā (šµ Ć š¶))) |
26 | | elxp7 7957 |
. . 3
ā¢ (š¤ ā (š“ Ć š¶) ā (š¤ ā (V Ć V) ā§ ((1st
āš¤) ā š“ ā§ (2nd
āš¤) ā š¶))) |
27 | 14, 25, 26 | 3bitr4g 314 |
. 2
ā¢ (š“ ā šµ ā (š¤ ā (ā”(1st ā¾ (šµ Ć š¶)) ā š“) ā š¤ ā (š“ Ć š¶))) |
28 | 27 | eqrdv 2731 |
1
ā¢ (š“ ā šµ ā (ā”(1st ā¾ (šµ Ć š¶)) ā š“) = (š“ Ć š¶)) |