![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3orbi123i | Structured version Visualization version GIF version |
Description: Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.) |
Ref | Expression |
---|---|
bi3.1 | ⊢ (𝜑 ↔ 𝜓) |
bi3.2 | ⊢ (𝜒 ↔ 𝜃) |
bi3.3 | ⊢ (𝜏 ↔ 𝜂) |
Ref | Expression |
---|---|
3orbi123i | ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi3.1 | . . . 4 ⊢ (𝜑 ↔ 𝜓) | |
2 | bi3.2 | . . . 4 ⊢ (𝜒 ↔ 𝜃) | |
3 | 1, 2 | orbi12i 914 | . . 3 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) |
4 | bi3.3 | . . 3 ⊢ (𝜏 ↔ 𝜂) | |
5 | 3, 4 | orbi12i 914 | . 2 ⊢ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) |
6 | df-3or 1089 | . 2 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜏)) | |
7 | df-3or 1089 | . 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) | |
8 | 5, 6, 7 | 3bitr4i 303 | 1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∨ wo 846 ∨ w3o 1087 |
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 1089 |
This theorem is referenced by: ne3anior 3035 otthne 5447 brtp 5484 wecmpep 5629 cnvso 6244 sorpss 7669 epweon 7713 epweonALT 7714 soxp 8065 dford2 9564 elfz0lmr 13696 sltsolem1 27046 axlowdimlem6 27945 elxrge02 31844 dfon2 34430 frege129d 42127 dfxlim2 44179 |
Copyright terms: Public domain | W3C validator |