![]() |
Mathbox for Jonathan Ben-Naim |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bnj17 | Structured version Visualization version Unicode version |
Description: Define the 4-way conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-bnj17 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph |
. . 3
![]() ![]() | |
2 | wps |
. . 3
![]() ![]() | |
3 | wch |
. . 3
![]() ![]() | |
4 | wth |
. . 3
![]() ![]() | |
5 | 1, 2, 3, 4 | w-bnj17 29539 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 2, 3 | w3a 991 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6, 4 | wa 375 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 5, 7 | wb 189 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: bnj248 29553 bnj250 29554 bnj258 29561 bnj268 29562 bnj291 29564 bnj312 29565 bnj446 29570 bnj645 29608 bnj658 29609 bnj887 29624 bnj919 29626 bnj945 29633 bnj951 29635 bnj982 29638 bnj1019 29639 bnj518 29745 bnj571 29765 bnj594 29771 bnj916 29792 bnj966 29803 bnj967 29804 bnj1006 29818 bnj1018 29821 bnj1040 29829 bnj1174 29860 bnj1175 29861 bnj1311 29881 |
Copyright terms: Public domain | W3C validator |