| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define conjunction ('and') of 3 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 633. |
| Ref | Expression |
|---|---|
| df-3an |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph |
. . 3
| |
| 2 | wps |
. . 3
| |
| 3 | wch |
. . 3
| |
| 4 | 1, 2, 3 | w3a 1102 |
. 2
|
| 5 | 1, 2 | wa 337 |
. . 3
|
| 6 | 5, 3 | wa 337 |
. 2
|
| 7 | 4, 6 | wb 219 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: 3anass 1106 3anrot 1107 3ancoma 1109 3anor 1113 3ioran 1115 3simpa 1117 3pm3.2i 1298 pm3.2an3 1299 3jca 1300 3anbi123i 1306 3imp 1311 3anbi123d 1441 3anim123d 1448 an6 1450 hb3an 1648 19.26-3an 1705 sb3an 1884 eeeanv 1975 mopick2 2099 3reeanv 2494 ceqsex3v 2575 ceqsex4v 2576 ceqsex8v 2578 tpss 3334 otthg 3698 poirr 3757 po3nr 3760 pofun 3763 wefrc 3806 dfwe2 4007 brinxp 4191 dff1o3 4728 f1orn 4732 dff1o6 4948 oprabid 5002 ndmoprass 5074 tz7.49cOLD 5334 tz7.49c 5336 oaord 5392 fiint 5872 abfii2 5874 alephval3 6233 sup2 7600 elioo3g 7893 eliooord 7902 rexuz2 7961 elfz2 8003 elfzuzb 8007 fznn0 8057 fznn 8058 expword2i 8234 abs2dif 8539 climcmplem 8793 isumcmpii 8872 mulc1cncf 8939 infxpidmlem7OLD 9221 divalglem8 9297 divalglem10 9299 divalgb 9301 exprmfctlem 9380 isbasis3g 9733 bl2in 9986 lmfval 10069 iscauf 10083 iscau5 10085 iscaunns 10088 nvex 10431 isnv 10432 sspval 10590 efifolem4 10950 axgroth3 11009 symgoprab 11033 hmph 11076 fbunfip 11120 flimff 11155 h2hcau 11319 dfadj2 12281 cnvadj 12285 adjeq 12328 eleigvec2 12351 irredi 12797 bnj169 12864 bnj170 12865 bnj171 12866 bnj172 12867 bnj173 12868 bnj178 12873 bnj248 12907 bnj252 12911 bnj253 12912 bnj180 13274 bnj512 13292 bnj574 13318 bnj856 13560 bnj861 13565 bnj945 13615 bnj962 13627 bnj980 13633 bnj1111 13695 bnj1224 13770 bnj109 13997 bnj129 14010 bnj149 14012 bnj153 14018 bnj557 14052 bnj571 14060 bnj849 14089 bnj986 14131 bnj996 14133 bnj1128 14199 bnj1174 14213 lediv2aALT 14413 elno3 14661 axfelem9 14707 ellimits 14771 r19.26t 14982 dff1o6f 15128 oprabval2gc 15188 oprabval4gc 15189 iscst1 15258 iscst2 15259 dmhmph 15643 rnhmph 15644 hmeogrp 15649 efilcp 15688 efilcp2 15692 cnfilca 15693 limfillem1 15704 grphmlem2 15770 grphlem3 15771 grphm 15774 ishoma 15930 ishomb 15931 isseg1 16114 isseg2 16115 compfipin0 16260 dfcon2 16266 fbasfip 16380 filssufillem 16394 fclsfnflim 16438 flimfnfcls 16439 fclusff 16447 3reeanvOLD 16485 pofunOLD 16596 fdc 16636 abl4pnp 16861 phtpcer 16886 pcoval 16897 pcoloopf 16903 crngm4 16975 isidlc 16987 pridl 17009 ispridl2 17010 ispridlc 17042 dfvd3 17325 3impexpVD 17514 cmtfval 17604 cmtval 17605 ishlat1 17748 ishlat2 17749 3dim0 17853 2dim 17866 islvol5 18011 cdleme0ex2 18593 cdleme0nex 18661 cdlemg2cex 18969 |