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 909 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
3 | orcom 864 | . 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓)) | |
4 | orcom 864 | . 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 315 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∨ wo 841 |
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 |
This theorem is referenced by: orbi1 911 orbi12d 912 eueq2 3698 uneq1 4129 r19.45zv 4444 rexprgf 4623 rextpg 4627 swopolem 5476 ordsseleq 6213 ordtri3 6220 infltoreq 8954 cantnflem1 9140 axgroth2 10235 axgroth3 10241 lelttric 10735 ltxr 12498 xmulneg1 12650 fzpr 12950 elfzp12 12974 caubnd 14706 lcmval 15924 lcmass 15946 isprm6 16046 vdwlem10 16314 irredmul 19388 domneq0 19998 opsrval 20183 znfld 20635 logreclem 25267 perfectlem2 25733 legov3 26311 lnhl 26328 colperpex 26446 lmif 26498 islmib 26500 friendshipgt3 28104 h1datom 29286 xrlelttric 30402 tlt3 30579 prmidl 30876 esumpcvgval 31236 sibfof 31497 satfvsuc 32505 satfv1 32507 satfvsucsuc 32509 satf0suc 32520 sat1el2xp 32523 fmlasuc0 32528 fmlafvel 32529 satfv1fvfmla1 32567 segcon2 33463 poimirlem25 34798 cnambfre 34821 pridl 35196 ismaxidl 35199 ispridlc 35229 pridlc 35230 dmnnzd 35234 4atlem3a 36613 pmapjoin 36868 lcfl3 38510 lcfl4N 38511 sbcoreleleqVD 41070 fourierdlem80 42348 euoreqb 43185 el1fzopredsuc 43402 perfectALTVlem2 43764 nnsum3primesle9 43836 lindslinindsimp2 44446 |
Copyright terms: Public domain | W3C validator |