Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3orbi123d | Structured version Visualization version GIF version |
Description: Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.) |
Ref | Expression |
---|---|
bi3d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
bi3d.2 | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
bi3d.3 | ⊢ (𝜑 → (𝜂 ↔ 𝜁)) |
Ref | Expression |
---|---|
3orbi123d | ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi3d.1 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | bi3d.2 | . . . 4 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
3 | 1, 2 | orbi12d 915 | . . 3 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏))) |
4 | bi3d.3 | . . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁)) | |
5 | 3, 4 | orbi12d 915 | . 2 ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁))) |
6 | df-3or 1084 | . 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) | |
7 | df-3or 1084 | . 2 ⊢ ((𝜒 ∨ 𝜏 ∨ 𝜁) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁)) | |
8 | 5, 6, 7 | 3bitr4g 316 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∨ wo 843 ∨ w3o 1082 |
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 209 df-or 844 df-3or 1084 |
This theorem is referenced by: moeq3 3703 soeq1 5489 solin 5493 soinxp 5628 ordtri3or 6218 isosolem 7094 sorpssi 7449 dfwe2 7490 f1oweALT 7667 soxp 7817 elfiun 8888 sornom 9693 ltsopr 10448 elz 11977 dyaddisj 24191 istrkgl 26238 istrkgld 26239 axtgupdim2 26251 tgdim01 26287 tglngval 26331 tgellng 26333 colcom 26338 colrot1 26339 legso 26379 lncom 26402 lnrot1 26403 lnrot2 26404 ttgval 26655 colinearalg 26690 axlowdim2 26740 axlowdim 26741 elntg 26764 elntg2 26765 nb3grprlem2 27157 frgrwopreg 28096 istrkg2d 31932 axtgupdim2ALTV 31934 brcolinear2 33514 colineardim1 33517 colinearperm1 33518 fin2so 34873 uneqsn 40366 3orbi123 40838 |
Copyright terms: Public domain | W3C validator |