![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3orass | Structured version Visualization version GIF version |
Description: Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.) |
Ref | Expression |
---|---|
3orass | ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3or 1081 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) | |
2 | orass 916 | . 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
3 | 1, 2 | bitri 276 | 1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∨ wo 842 ∨ w3o 1079 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 208 df-or 843 df-3or 1081 |
This theorem is referenced by: 3orel1 1084 3orrot 1085 3orcoma 1086 3mix1 1323 ecase23d 1465 3bior1fd 1467 cador 1590 moeq3 3639 sotric 5389 sotrieq 5390 isso2i 5396 ordzsl 7416 soxp 7676 wemapsolem 8860 rankxpsuc 9157 tcrank 9159 cardlim 9247 cardaleph 9361 grur1 10088 elnnz 11839 elznn0 11844 elznn 11845 elxr 12361 xrrebnd 12411 xaddf 12467 xrinfmss 12553 elfzlmr 13001 ssnn0fi 13203 hashv01gt1 13555 hashtpg 13689 swrdnd2 13853 pfxnd0 13886 tgldimor 25970 outpasch 26223 xrdifh 30191 eliccioo 30291 orngsqr 30531 elzdif0 30838 qqhval2lem 30839 dfso2 32598 dfon2lem5 32640 dfon2lem6 32641 nofv 32773 nosepon 32781 ecase13d 33270 elicc3 33274 wl-exeq 34306 dvasin 34509 4atlem3a 36264 4atlem3b 36265 frege133d 39595 or3or 39856 3ornot23VD 40720 xrssre 41157 |
Copyright terms: Public domain | W3C validator |