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 381. (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 885 | . 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
5 | 1, 2 | wa 97 | . . 3 wff (𝜑 ∧ 𝜓) |
6 | 5, 3 | wa 97 | . 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒) |
7 | 4, 6 | wb 98 | 1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
Colors of variables: wff set class |
This definition is referenced by: 3anass 889 3anrot 890 3ancoma 892 3anan32 896 3ioran 900 3simpa 901 3pm3.2i 1082 pm3.2an3 1083 3jca 1084 3anbi123i 1093 3imp 1098 3anbi123d 1207 3anim123d 1214 an6 1216 19.26-3an 1372 hb3an 1442 nf3an 1458 nf3and 1461 eeeanv 1808 sb3an 1832 mopick2 1983 r19.26-3 2443 3reeanv 2480 ceqsex3v 2596 ceqsex4v 2597 ceqsex8v 2599 elin3 3128 raltpg 3423 tpss 3529 dfopg 3547 opeq1 3549 opeq2 3550 opm 3971 otth2 3978 poirr 4044 po3nr 4047 wepo 4096 wetrep 4097 rabxp 4380 brinxp2 4407 brinxp 4408 sotri2 4722 sotri3 4723 f1orn 5136 dff1o6 5416 isosolem 5463 oprabid 5537 caovimo 5694 elovmpt2 5701 dfxp3 5820 nnaord 6082 prmuloc 6664 ltrelxr 7080 rexuz2 8524 ltxr 8695 elixx3g 8770 elioo4g 8803 elioopnf 8836 elioomnf 8837 elicopnf 8838 elxrge0 8847 divelunit 8870 elfz2 8881 elfzuzb 8884 uzsplit 8954 fznn0 8974 elfzmlbp 8990 elfzo2 9007 fzolb2 9010 fzouzsplit 9035 ssfzo12bi 9081 fzind2 9095 abs2dif 9702 bd3an 9950 |
Copyright terms: Public domain | W3C validator |