| 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 915 | . . 3 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) |
| 4 | bi3.3 | . . 3 ⊢ (𝜏 ↔ 𝜂) | |
| 5 | 3, 4 | orbi12i 915 | . 2 ⊢ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) |
| 6 | df-3or 1088 | . 2 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜏)) | |
| 7 | df-3or 1088 | . 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) | |
| 8 | 5, 6, 7 | 3bitr4i 303 | 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: ne3anior 3036 otthne 5491 brtp 5528 wecmpep 5677 cnvso 6308 sorpss 7748 epweon 7795 epweonALT 7796 soxp 8154 dford2 9660 elfz0lmr 13821 hash3tpde 14532 sltsolem1 27720 axlowdimlem6 28962 elxrge02 32914 dfon2 35793 frege129d 43776 dfxlim2 45863 usgrexmpl2trifr 47996 |
| Copyright terms: Public domain | W3C validator |