![]() |
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 911 | . . 3 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) |
4 | bi3.3 | . . 3 ⊢ (𝜏 ↔ 𝜂) | |
5 | 3, 4 | orbi12i 911 | . 2 ⊢ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) |
6 | df-3or 1086 | . 2 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜏)) | |
7 | df-3or 1086 | . 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) | |
8 | 5, 6, 7 | 3bitr4i 302 | 1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∨ wo 843 ∨ 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 844 df-3or 1086 |
This theorem is referenced by: ne3anior 3034 otthne 5485 brtp 5522 wecmpep 5667 cnvso 6286 sorpss 7720 epweon 7764 epweonALT 7765 soxp 8117 dford2 9617 elfz0lmr 13751 sltsolem1 27414 axlowdimlem6 28472 elxrge02 32365 dfon2 35068 frege129d 42816 dfxlim2 44862 |
Copyright terms: Public domain | W3C validator |