![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orbi1d | Structured version Visualization version GIF version |
Description: Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
bid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
orbi1d | ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bid.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | orbi2d 944 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
3 | orcom 901 | . 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓)) | |
4 | orcom 901 | . 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 306 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∨ wo 878 |
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 |
This theorem is referenced by: orbi1 946 orbi12d 947 eueq2 3605 uneq1 3987 r19.45zv 4290 rexprg 4454 rextpg 4456 swopolem 5272 ordsseleq 5992 ordtri3 5999 infltoreq 8677 cantnflem1 8863 axgroth2 9962 axgroth3 9968 lelttric 10463 ltxr 12235 xmulneg1 12387 fzpr 12689 elfzp12 12713 caubnd 14475 lcmval 15678 lcmass 15700 isprm6 15797 vdwlem10 16065 irredmul 19063 domneq0 19658 opsrval 19835 znfld 20268 logreclem 24902 perfectlem2 25368 legov3 25910 lnhl 25927 colperpex 26042 lmif 26094 islmib 26096 friendshipgt3 27802 h1datom 28985 xrlelttric 30053 tlt3 30199 esumpcvgval 30674 sibfof 30936 segcon2 32740 poimirlem25 33971 cnambfre 33994 pridl 34371 ismaxidl 34374 ispridlc 34404 pridlc 34405 dmnnzd 34409 4atlem3a 35665 pmapjoin 35920 lcfl3 37562 lcfl4N 37563 sbcoreleleqVD 39906 fourierdlem80 41190 el1fzopredsuc 42216 perfectALTVlem2 42454 nnsum3primesle9 42505 lindslinindsimp2 43092 |
Copyright terms: Public domain | W3C validator |