![]() |
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 1086 | . 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) | |
2 | orass 920 | . 2 ⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | |
3 | 1, 2 | bitri 275 | 1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∨ wo 846 ∨ w3o 1084 |
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 206 df-or 847 df-3or 1086 |
This theorem is referenced by: 3orel1 1089 3orrot 1090 3orcoma 1091 3mix1 1328 ecase23d 1470 3bior1fd 1472 cador 1602 moeq3 3707 sotric 5618 sotrieq 5619 isso2i 5625 ordzsl 7849 soxp 8134 frxp3 8156 wemapsolem 9574 rankxpsuc 9906 tcrank 9908 cardlim 9996 cardaleph 10113 grur1 10844 elnnz 12599 elznn0 12604 elznn 12605 elxr 13129 xrrebnd 13180 xaddf 13236 xrinfmss 13322 elfzlmr 13779 ssnn0fi 13983 hashv01gt1 14337 hashtpg 14479 swrdnd2 14638 pfxnd0 14671 nofv 27603 nosepon 27611 tgldimor 28319 outpasch 28572 xrdifh 32561 eliccioo 32667 orngsqr 33032 elzdif0 33581 qqhval2lem 33582 dfso2 35349 dfon2lem5 35383 dfon2lem6 35384 ecase13d 35797 elicc3 35801 wl-df4-3mintru2 36966 wl-exeq 37001 dvasin 37177 4atlem3a 39070 4atlem3b 39071 frege133d 43195 or3or 43453 3ornot23VD 44286 xrssre 44730 |
Copyright terms: Public domain | W3C validator |