![]() |
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 947 | . . 3 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏))) |
4 | bi3d.3 | . . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁)) | |
5 | 3, 4 | orbi12d 947 | . 2 ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁))) |
6 | df-3or 1112 | . 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂)) | |
7 | df-3or 1112 | . 2 ⊢ ((𝜒 ∨ 𝜏 ∨ 𝜁) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁)) | |
8 | 5, 6, 7 | 3bitr4g 306 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∨ wo 878 ∨ w3o 1110 |
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 199 df-or 879 df-3or 1112 |
This theorem is referenced by: moeq3 3608 soeq1 5285 solin 5289 soinxp 5422 ordtri3or 5999 isosolem 6857 sorpssi 7208 dfwe2 7247 f1oweALT 7417 soxp 7559 elfiun 8611 sornom 9421 ltsopr 10176 elz 11713 dyaddisj 23769 istrkgl 25777 istrkgld 25778 axtgupdim2 25790 tgdim01 25826 tglngval 25870 tgellng 25872 colcom 25877 colrot1 25878 legso 25918 lncom 25941 lnrot1 25942 lnrot2 25943 ttgval 26181 colinearalg 26216 axlowdim2 26266 axlowdim 26267 elntg 26290 elntg2 26291 nb3grprlem2 26686 frgrwopreg 27700 istrkg2d 31289 axtgupdim2OLD 31291 brcolinear2 32699 colineardim1 32702 colinearperm1 32703 fin2so 33934 uneqsn 39156 3orbi123 39550 |
Copyright terms: Public domain | W3C validator |