![]() |
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 393. (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 920 | . 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
5 | 1, 2 | wa 102 | . . 3 wff (𝜑 ∧ 𝜓) |
6 | 5, 3 | wa 102 | . 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒) |
7 | 4, 6 | wb 103 | 1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
Colors of variables: wff set class |
This definition is referenced by: 3anass 924 3anrot 925 3ancoma 927 3anan32 931 3ioran 935 3simpa 936 3pm3.2i 1117 pm3.2an3 1118 3jca 1119 3anbi123i 1128 3imp 1133 3anbi123d 1244 3anim123d 1251 an6 1253 19.26-3an 1413 hb3an 1483 nf3an 1499 nf3and 1502 eeeanv 1850 sb3an 1874 mopick2 2025 r19.26-3 2488 3reeanv 2525 ceqsex3v 2642 ceqsex4v 2643 ceqsex8v 2645 sbc3an 2876 elin3 3164 raltpg 3453 tpss 3558 dfopg 3576 opeq1 3578 opeq2 3579 opm 3997 otth2 4004 poirr 4070 po3nr 4073 wepo 4122 wetrep 4123 rabxp 4406 brinxp2 4433 brinxp 4434 sotri2 4752 sotri3 4753 f1orn 5167 dff1o6 5447 isosolem 5494 oprabid 5568 caovimo 5725 elovmpt2 5732 dfxp3 5851 nnaord 6148 prmuloc 6818 ltrelxr 7240 rexuz2 8750 ltxr 8927 elixx3g 9000 elioo4g 9033 elioopnf 9066 elioomnf 9067 elicopnf 9068 elxrge0 9077 divelunit 9100 elfz2 9112 elfzuzb 9115 uzsplit 9185 fznn0 9206 elfzmlbp 9220 elfzo2 9237 fzolb2 9240 fzouzsplit 9265 ssfzo12bi 9311 fzind2 9325 abs2dif 10130 sumeq2d 10334 sumeq2 10335 divalgb 10469 divgcdz 10507 rplpwr 10560 cncongr1 10629 bd3an 10779 |
Copyright terms: Public domain | W3C validator |