![]() |
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 401. (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 978 | . 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
5 | 1, 2 | wa 104 | . . 3 wff (𝜑 ∧ 𝜓) |
6 | 5, 3 | wa 104 | . 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒) |
7 | 4, 6 | wb 105 | 1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
Colors of variables: wff set class |
This definition is referenced by: 3anass 982 3anrot 983 3ancoma 985 3anan32 989 3ioran 993 3simpa 994 3pm3.2i 1175 pm3.2an3 1176 3jca 1177 3anbi123i 1188 3imp 1193 3anbi123d 1312 3anim123d 1319 an6 1321 19.26-3an 1483 hb3an 1550 nf3an 1566 nf3and 1569 eeeanv 1933 sb3an 1958 mopick2 2109 r19.26-3 2607 3reeanv 2647 ceqsex3v 2779 ceqsex4v 2780 ceqsex8v 2782 sbc3an 3024 elin3 3326 rexdifpr 3620 raltpg 3645 tpss 3758 dfopg 3776 opeq1 3778 opeq2 3779 opm 4234 otth2 4241 poirr 4307 po3nr 4310 wepo 4359 wetrep 4360 rabxp 4663 brinxp2 4693 brinxp 4694 sotri2 5026 sotri3 5027 f1orn 5471 dff1o6 5776 isosolem 5824 oprabid 5906 caovimo 6067 elovmpo 6071 dfxp3 6194 nnaord 6509 fiintim 6927 prmuloc 7564 ltrelxr 8017 rexuz2 9580 ltxr 9774 elixx3g 9900 elioo4g 9933 elioopnf 9966 elioomnf 9967 elicopnf 9968 elxrge0 9977 divelunit 10001 elfz2 10014 elfzuzb 10018 uzsplit 10091 fznn0 10112 elfzmlbp 10131 elfzo2 10149 fzolb2 10153 fzouzsplit 10178 ssfzo12bi 10224 fzind2 10238 dfrp2 10263 abs2dif 11114 sumeq2 11366 divalgb 11929 divgcdz 11971 rplpwr 12027 nnwosdc 12039 cncongr1 12102 pythagtriplem2 12265 pythagtrip 12282 xpscf 12765 issubm2 12863 issubg3 13050 resgrpisgrp 13053 eqgval 13080 eqger 13081 ringpropd 13215 isbasis3g 13516 lmfval 13662 lmbr 13683 lmbr2 13684 xmeterval 13905 xmeter 13906 cnbl0 14004 cnblcld 14005 limcrcl 14097 bd3an 14552 |
Copyright terms: Public domain | W3C validator |