Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-3an | GIF 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 398. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
df-3an | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | wps | . . 3 wff 𝜓 | |
3 | wch | . . 3 wff 𝜒 | |
4 | 1, 2, 3 | w3a 947 | . 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
5 | 1, 2 | wa 103 | . . 3 wff (𝜑 ∧ 𝜓) |
6 | 5, 3 | wa 103 | . 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒) |
7 | 4, 6 | wb 104 | 1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
Colors of variables: wff set class |
This definition is referenced by: 3anass 951 3anrot 952 3ancoma 954 3anan32 958 3ioran 962 3simpa 963 3pm3.2i 1144 pm3.2an3 1145 3jca 1146 3anbi123i 1155 3imp 1160 3anbi123d 1275 3anim123d 1282 an6 1284 19.26-3an 1444 hb3an 1514 nf3an 1530 nf3and 1533 eeeanv 1885 sb3an 1909 mopick2 2060 r19.26-3 2539 3reeanv 2578 ceqsex3v 2702 ceqsex4v 2703 ceqsex8v 2705 sbc3an 2942 elin3 3237 raltpg 3546 tpss 3655 dfopg 3673 opeq1 3675 opeq2 3676 opm 4126 otth2 4133 poirr 4199 po3nr 4202 wepo 4251 wetrep 4252 rabxp 4546 brinxp2 4576 brinxp 4577 sotri2 4906 sotri3 4907 f1orn 5345 dff1o6 5645 isosolem 5693 oprabid 5771 caovimo 5932 elovmpo 5939 dfxp3 6060 nnaord 6373 fiintim 6785 prmuloc 7342 ltrelxr 7793 rexuz2 9332 ltxr 9517 elixx3g 9639 elioo4g 9672 elioopnf 9705 elioomnf 9706 elicopnf 9707 elxrge0 9716 divelunit 9740 elfz2 9752 elfzuzb 9755 uzsplit 9827 fznn0 9848 elfzmlbp 9864 elfzo2 9882 fzolb2 9886 fzouzsplit 9911 ssfzo12bi 9957 fzind2 9971 abs2dif 10833 sumeq2 11083 divalgb 11534 divgcdz 11572 rplpwr 11627 cncongr1 11696 isbasis3g 12124 lmfval 12272 lmbr 12293 lmbr2 12294 xmeterval 12515 xmeter 12516 cnbl0 12614 cnblcld 12615 limcrcl 12707 bd3an 12924 |
Copyright terms: Public domain | W3C validator |