![]() |
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 884 | . 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 888 3anrot 889 3ancoma 891 3anan32 895 3ioran 899 3simpa 900 3pm3.2i 1081 pm3.2an3 1082 3jca 1083 3anbi123i 1092 3imp 1097 3anbi123d 1206 3anim123d 1213 an6 1215 19.26-3an 1369 hb3an 1439 nf3an 1455 nf3and 1458 eeeanv 1805 sb3an 1829 mopick2 1980 r19.26-3 2437 3reeanv 2474 ceqsex3v 2590 ceqsex4v 2591 ceqsex8v 2593 elin3 3122 raltpg 3414 tpss 3520 dfopg 3538 opeq1 3540 opeq2 3541 opm 3962 otth2 3969 poirr 4035 po3nr 4038 rabxp 4323 brinxp2 4350 brinxp 4351 sotri2 4665 sotri3 4666 f1orn 5079 dff1o6 5359 isosolem 5406 oprabid 5480 caovimo 5636 elovmpt2 5643 dfxp3 5762 nnaord 6018 prmuloc 6547 ltrelxr 6877 rexuz2 8300 ltxr 8465 elixx3g 8540 elioo4g 8573 elioopnf 8606 elioomnf 8607 elicopnf 8608 elxrge0 8617 divelunit 8640 elfz2 8651 elfzuzb 8654 uzsplit 8724 fznn0 8744 elfzmlbp 8760 elfzo2 8777 fzolb2 8780 fzouzsplit 8805 ssfzo12bi 8851 fzind2 8865 bd3an 9285 |
Copyright terms: Public domain | W3C validator |