| 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 919 | . . 3 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏))) |
| 4 | bi3d.3 | . . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁)) | |
| 5 | 3, 4 | orbi12d 919 | . 2 ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁))) |
| 6 | df-3or 1088 | . 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) | |
| 7 | df-3or 1088 | . 2 ⊢ ((𝜒 ∨ 𝜏 ∨ 𝜁) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁)) | |
| 8 | 5, 6, 7 | 3bitr4g 314 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ 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: moeq3 3718 soeq1 5613 solin 5619 soinxp 5767 ordtri3or 6416 isosolem 7367 sorpssi 7749 dfwe2 7794 f1oweALT 7997 soxp 8154 frxp3 8176 xpord3inddlem 8179 elfiun 9470 sornom 10317 ltsopr 11072 elz 12615 dyaddisj 25631 istrkgl 28466 istrkgld 28467 axtgupdim2 28479 tgdim01 28515 tglngval 28559 tgellng 28561 colcom 28566 colrot1 28567 legso 28607 lncom 28630 lnrot1 28631 lnrot2 28632 ttgval 28883 ttgvalOLD 28884 colinearalg 28925 axlowdim2 28975 axlowdim 28976 elntg 28999 elntg2 29000 nb3grprlem2 29398 frgrwopreg 30342 constrsuc 33779 istrkg2d 34681 axtgupdim2ALTV 34683 brcolinear2 36059 colineardim1 36062 colinearperm1 36063 fin2so 37614 uneqsn 44038 3orbi123 44531 gpgov 48001 gpgedgel 48007 gpgedgvtx0 48019 gpgedgvtx1 48020 gpg3kgrtriexlem6 48044 |
| Copyright terms: Public domain | W3C validator |