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 912 | . . 3 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏))) |
4 | bi3d.3 | . . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁)) | |
5 | 3, 4 | orbi12d 912 | . 2 ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁))) |
6 | df-3or 1080 | . 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) | |
7 | df-3or 1080 | . 2 ⊢ ((𝜒 ∨ 𝜏 ∨ 𝜁) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁)) | |
8 | 5, 6, 7 | 3bitr4g 315 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∨ wo 841 ∨ w3o 1078 |
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 208 df-or 842 df-3or 1080 |
This theorem is referenced by: moeq3 3700 soeq1 5487 solin 5491 soinxp 5626 ordtri3or 6216 isosolem 7089 sorpssi 7444 dfwe2 7485 f1oweALT 7662 soxp 7812 elfiun 8882 sornom 9687 ltsopr 10442 elz 11971 dyaddisj 24124 istrkgl 26171 istrkgld 26172 axtgupdim2 26184 tgdim01 26220 tglngval 26264 tgellng 26266 colcom 26271 colrot1 26272 legso 26312 lncom 26335 lnrot1 26336 lnrot2 26337 ttgval 26588 colinearalg 26623 axlowdim2 26673 axlowdim 26674 elntg 26697 elntg2 26698 nb3grprlem2 27090 frgrwopreg 28029 istrkg2d 31836 axtgupdim2ALTV 31838 brcolinear2 33416 colineardim1 33419 colinearperm1 33420 fin2so 34760 uneqsn 40251 3orbi123 40722 |
Copyright terms: Public domain | W3C validator |