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 742 | . . 3 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏))) |
4 | bi3d.3 | . . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁)) | |
5 | 3, 4 | orbi12d 742 | . 2 ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁))) |
6 | df-3or 1032 | . 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) | |
7 | df-3or 1032 | . 2 ⊢ ((𝜒 ∨ 𝜏 ∨ 𝜁) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁)) | |
8 | 5, 6, 7 | 3bitr4g 302 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∨ wo 382 ∨ w3o 1030 |
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 196 df-or 384 df-3or 1032 |
This theorem is referenced by: moeq3 3350 soeq1 4978 solin 4982 soinxp 5106 ordtri3or 5672 isosolem 6497 sorpssi 6841 dfwe2 6873 f1oweALT 7043 soxp 7177 elfiun 8219 sornom 8982 ltsopr 9733 elz 11256 dyaddisj 23170 istrkgl 25157 istrkgld 25158 axtgupdim2 25170 tgdim01 25202 tglngval 25246 tgellng 25248 colcom 25253 colrot1 25254 legso 25294 lncom 25317 lnrot1 25318 lnrot2 25319 ttgval 25555 colinearalg 25590 axlowdim2 25640 axlowdim 25641 elntg 25664 nb3graprlem2 25981 frgraregorufr0 26579 istrkg2d 29997 axtgupdim2OLD 29999 brcolinear2 31335 colineardim1 31338 colinearperm1 31339 fin2so 32566 uneqsn 37341 3orbi123 37738 nb3grprlem2 40609 frgrregorufr0 41489 |
Copyright terms: Public domain | W3C validator |