![]() |
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 912 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
3 | orcom 867 | . 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓)) | |
4 | orcom 867 | . 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∨ wo 844 |
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 845 |
This theorem is referenced by: orbi1 914 orbi12d 915 eueq2 3698 uneq1 4148 r19.45zv 4494 rexprgf 4689 rextpg 4695 swopolem 5588 ordsseleq 6383 ordtri3 6390 frxp2 8124 xpord2pred 8125 xpord2indlem 8127 frxp3 8131 xpord3pred 8132 infltoreq 9493 cantnflem1 9680 axgroth2 10816 axgroth3 10822 lelttric 11318 ltxr 13092 xmulneg1 13245 fzpr 13553 elfzp12 13577 caubnd 15302 lcmval 16526 lcmass 16548 isprm6 16648 vdwlem10 16922 irredmul 20321 lringuplu 20434 domneq0 21197 znfld 21423 opsrval 21911 logreclem 26610 perfectlem2 27079 legov3 28318 lnhl 28335 colperpex 28453 lmif 28505 islmib 28507 friendshipgt3 30120 h1datom 31304 xrlelttric 32434 tlt3 32607 prmidl 33027 ismxidl 33047 esumpcvgval 33565 sibfof 33828 satfvsuc 34841 satfv1 34843 satfvsucsuc 34845 satf0suc 34856 sat1el2xp 34859 fmlasuc0 34864 fmlafvel 34865 satfv1fvfmla1 34903 segcon2 35572 wl-ifpimpr 36837 poimirlem25 37003 cnambfre 37026 pridl 37395 ismaxidl 37398 ispridlc 37428 pridlc 37429 dmnnzd 37433 disjecxrncnvep 37750 4atlem3a 38958 pmapjoin 39213 lcfl3 40855 lcfl4N 40856 sticksstones22 41477 ordsssucb 42574 sbcoreleleqVD 44109 fourierdlem80 45387 euoreqb 46302 el1fzopredsuc 46518 perfectALTVlem2 46875 nnsum3primesle9 46947 lindslinindsimp2 47332 |
Copyright terms: Public domain | W3C validator |