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 399. (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 973 | . 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 977 3anrot 978 3ancoma 980 3anan32 984 3ioran 988 3simpa 989 3pm3.2i 1170 pm3.2an3 1171 3jca 1172 3anbi123i 1183 3imp 1188 3anbi123d 1307 3anim123d 1314 an6 1316 19.26-3an 1476 hb3an 1543 nf3an 1559 nf3and 1562 eeeanv 1926 sb3an 1951 mopick2 2102 r19.26-3 2600 3reeanv 2640 ceqsex3v 2772 ceqsex4v 2773 ceqsex8v 2775 sbc3an 3016 elin3 3318 rexdifpr 3611 raltpg 3636 tpss 3745 dfopg 3763 opeq1 3765 opeq2 3766 opm 4219 otth2 4226 poirr 4292 po3nr 4295 wepo 4344 wetrep 4345 rabxp 4648 brinxp2 4678 brinxp 4679 sotri2 5008 sotri3 5009 f1orn 5452 dff1o6 5755 isosolem 5803 oprabid 5885 caovimo 6046 elovmpo 6050 dfxp3 6173 nnaord 6488 fiintim 6906 prmuloc 7528 ltrelxr 7980 rexuz2 9540 ltxr 9732 elixx3g 9858 elioo4g 9891 elioopnf 9924 elioomnf 9925 elicopnf 9926 elxrge0 9935 divelunit 9959 elfz2 9972 elfzuzb 9975 uzsplit 10048 fznn0 10069 elfzmlbp 10088 elfzo2 10106 fzolb2 10110 fzouzsplit 10135 ssfzo12bi 10181 fzind2 10195 dfrp2 10220 abs2dif 11070 sumeq2 11322 divalgb 11884 divgcdz 11926 rplpwr 11982 nnwosdc 11994 cncongr1 12057 pythagtriplem2 12220 pythagtrip 12237 isbasis3g 12838 lmfval 12986 lmbr 13007 lmbr2 13008 xmeterval 13229 xmeter 13230 cnbl0 13328 cnblcld 13329 limcrcl 13421 bd3an 13865 |
Copyright terms: Public domain | W3C validator |