![]() |
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 916 | . . 3 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏))) |
4 | bi3d.3 | . . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁)) | |
5 | 3, 4 | orbi12d 916 | . 2 ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁))) |
6 | df-3or 1085 | . 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) | |
7 | df-3or 1085 | . 2 ⊢ ((𝜒 ∨ 𝜏 ∨ 𝜁) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁)) | |
8 | 5, 6, 7 | 3bitr4g 313 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∨ wo 845 ∨ w3o 1083 |
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 206 df-or 846 df-3or 1085 |
This theorem is referenced by: moeq3 3706 soeq1 5615 solin 5619 soinxp 5763 ordtri3or 6408 isosolem 7359 sorpssi 7740 dfwe2 7782 f1oweALT 7986 soxp 8143 frxp3 8165 xpord3inddlem 8168 elfiun 9473 sornom 10320 ltsopr 11075 elz 12612 dyaddisj 25616 istrkgl 28385 istrkgld 28386 axtgupdim2 28398 tgdim01 28434 tglngval 28478 tgellng 28480 colcom 28485 colrot1 28486 legso 28526 lncom 28549 lnrot1 28550 lnrot2 28551 ttgval 28802 ttgvalOLD 28803 colinearalg 28844 axlowdim2 28894 axlowdim 28895 elntg 28918 elntg2 28919 nb3grprlem2 29317 frgrwopreg 30256 constrsuc 33596 istrkg2d 34512 axtgupdim2ALTV 34514 brcolinear2 35882 colineardim1 35885 colinearperm1 35886 fin2so 37308 uneqsn 43692 3orbi123 44187 |
Copyright terms: Public domain | W3C validator |