![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > df-3an | Unicode version |
Description: Define conjunction ('and') of three wff's. Definition *4.34 of [WhiteheadRussell] p. 118. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law anass 630. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
df-3an |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph |
. . 3
![]() ![]() | |
2 | wps |
. . 3
![]() ![]() | |
3 | wch |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | w3a 934 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2 | wa 358 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5, 3 | wa 358 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wb 176 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: 3anass 938 3anrot 939 3ancoma 941 3anan32 946 3anor 948 3ioran 950 3simpa 952 3pm3.2i 1130 pm3.2an3 1131 3jca 1132 3anbi123i 1140 3imp 1145 3anbi123d 1252 3anim123d 1259 an6 1261 cadan 1392 19.26-3an 1595 nf3and 1823 nf3an 1827 hb3anOLD 1831 eeeanv 1914 sb3an 2070 mopick2 2271 r19.26-3 2748 3reeanv 2779 ceqsex3v 2897 ceqsex4v 2898 ceqsex8v 2900 elin3 3447 raltpg 3777 tpss 3871 sikexlem 4295 dfpw12 4301 srelk 4524 br1stg 4730 elswap 4740 rabxp 4814 brinxp2 4835 brinxp 4836 brswap2 4860 dff1o3 5292 f1orn 5296 dff1o6 5475 oprabid 5550 eloprabga 5578 ndmovass 5618 dmpprod 5840 trrd 5925 porta 5933 lecex 6115 ovcelem1 6171 sbthlem3 6205 addccan2nclem1 6263 nmembers1lem1 6268 spacvallem1 6281 nchoicelem17 6305 |
Copyright terms: Public domain | W3C validator |