![]() |
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 396. (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 930 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2 | wa 103 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5, 3 | wa 103 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wb 104 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 3anass 934 3anrot 935 3ancoma 937 3anan32 941 3ioran 945 3simpa 946 3pm3.2i 1127 pm3.2an3 1128 3jca 1129 3anbi123i 1138 3imp 1143 3anbi123d 1258 3anim123d 1265 an6 1267 19.26-3an 1427 hb3an 1497 nf3an 1513 nf3and 1516 eeeanv 1868 sb3an 1892 mopick2 2043 r19.26-3 2521 3reeanv 2559 ceqsex3v 2683 ceqsex4v 2684 ceqsex8v 2686 sbc3an 2922 elin3 3214 raltpg 3523 tpss 3632 dfopg 3650 opeq1 3652 opeq2 3653 opm 4094 otth2 4101 poirr 4167 po3nr 4170 wepo 4219 wetrep 4220 rabxp 4514 brinxp2 4544 brinxp 4545 sotri2 4872 sotri3 4873 f1orn 5311 dff1o6 5609 isosolem 5657 oprabid 5735 caovimo 5896 elovmpo 5903 dfxp3 6022 nnaord 6335 fiintim 6746 prmuloc 7275 ltrelxr 7697 rexuz2 9226 ltxr 9403 elixx3g 9525 elioo4g 9558 elioopnf 9591 elioomnf 9592 elicopnf 9593 elxrge0 9602 divelunit 9626 elfz2 9638 elfzuzb 9641 uzsplit 9713 fznn0 9734 elfzmlbp 9750 elfzo2 9768 fzolb2 9772 fzouzsplit 9797 ssfzo12bi 9843 fzind2 9857 abs2dif 10718 sumeq2 10967 divalgb 11417 divgcdz 11455 rplpwr 11508 cncongr1 11577 isbasis3g 11995 lmfval 12143 lmbr 12163 lmbr2 12164 xmeterval 12363 xmeter 12364 cnbl0 12456 cnblcld 12457 limcrcl 12509 bd3an 12609 |
Copyright terms: Public domain | W3C validator |