![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-3an | 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 401. (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 979 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2 | wa 104 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5, 3 | wa 104 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 3anass 983 3anrot 984 3ancoma 986 3anan32 990 3ioran 994 3simpa 995 3pm3.2i 1176 pm3.2an3 1177 3jca 1178 3anbi123i 1189 3imp 1194 3anbi123d 1322 3anim123d 1329 an6 1331 19.26-3an 1493 hb3an 1560 nf3an 1576 nf3and 1579 eeeanv 1943 sb3an 1968 mopick2 2119 r19.26-3 2617 3reeanv 2658 ceqsex3v 2791 ceqsex4v 2792 ceqsex8v 2794 sbc3an 3036 elin3 3338 rexdifpr 3632 raltpg 3657 tpss 3770 dfopg 3788 opeq1 3790 opeq2 3791 opm 4246 otth2 4253 poirr 4319 po3nr 4322 wepo 4371 wetrep 4372 rabxp 4675 brinxp2 4705 brinxp 4706 sotri2 5038 sotri3 5039 f1orn 5483 dff1o6 5790 isosolem 5838 oprabid 5920 caovimo 6082 elovmpo 6086 dfxp3 6209 nnaord 6524 fiintim 6942 prmuloc 7579 ltrelxr 8032 rexuz2 9595 ltxr 9789 elixx3g 9915 elioo4g 9948 elioopnf 9981 elioomnf 9982 elicopnf 9983 elxrge0 9992 divelunit 10016 elfz2 10029 elfzuzb 10033 uzsplit 10106 fznn0 10127 elfzmlbp 10146 elfzo2 10164 fzolb2 10168 fzouzsplit 10193 ssfzo12bi 10239 fzind2 10253 dfrp2 10278 abs2dif 11129 sumeq2 11381 divalgb 11944 divgcdz 11986 rplpwr 12042 nnwosdc 12054 cncongr1 12117 pythagtriplem2 12280 pythagtrip 12297 xpscf 12785 issgrpd 12837 issubm2 12886 issubg3 13092 resgrpisgrp 13095 eqgval 13123 eqger 13124 eqgabl 13222 qusecsub 13223 rnglz 13254 rngpropd 13264 ringpropd 13347 isbasis3g 13899 lmfval 14045 lmbr 14066 lmbr2 14067 xmeterval 14288 xmeter 14289 cnbl0 14387 cnblcld 14388 limcrcl 14480 bd3an 14935 |
Copyright terms: Public domain | W3C validator |