| 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 1088 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) | |
| 2 | orass 922 | . 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
| 3 | 1, 2 | bitri 275 | 1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∨ wo 848 ∨ w3o 1086 |
| 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 207 df-or 849 df-3or 1088 |
| This theorem is referenced by: 3orel1 1091 3orrot 1092 3orcoma 1093 3mix1 1331 ecase23d 1475 3bior1fd 1477 cador 1608 moeq3 3718 sotric 5622 sotrieq 5623 isso2i 5629 ordzsl 7866 soxp 8154 frxp3 8176 wemapsolem 9590 rankxpsuc 9922 tcrank 9924 cardlim 10012 cardaleph 10129 grur1 10860 elnnz 12623 elznn0 12628 elznn 12629 elxr 13158 xrrebnd 13210 xaddf 13266 xrinfmss 13352 elfzlmr 13820 ssnn0fi 14026 hashv01gt1 14384 hashtpg 14524 swrdnd2 14693 pfxnd0 14726 nofv 27702 nosepon 27710 elzs2 28385 elnnzs 28387 elznns 28388 tgldimor 28510 outpasch 28763 xrdifh 32782 eliccioo 32913 orngsqr 33334 elzdif0 33981 qqhval2lem 33982 dfso2 35755 dfon2lem5 35788 dfon2lem6 35789 ecase13d 36314 elicc3 36318 wl-df4-3mintru2 37488 wl-exeq 37535 dvasin 37711 4atlem3a 39599 4atlem3b 39600 frege133d 43778 or3or 44036 3ornot23VD 44867 xrssre 45359 usgrexmpl2nb0 47990 usgrexmpl2nb2 47992 usgrexmpl2nb3 47993 usgrexmpl2nb5 47995 |
| Copyright terms: Public domain | W3C validator |