![]() |
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 1087 | . 2 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜏)) | |
7 | df-3or 1087 | . 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) | |
8 | 5, 6, 7 | 3bitr4i 303 | 1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∨ wo 847 ∨ w3o 1085 |
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 848 df-3or 1087 |
This theorem is referenced by: ne3anior 3034 otthne 5497 brtp 5533 wecmpep 5681 cnvso 6310 sorpss 7747 epweon 7794 epweonALT 7795 soxp 8153 dford2 9658 elfz0lmr 13818 hash3tpde 14529 sltsolem1 27735 axlowdimlem6 28977 elxrge02 32899 dfon2 35774 frege129d 43753 dfxlim2 45804 usgrexmpl2trifr 47932 |
Copyright terms: Public domain | W3C validator |