![]() |
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 738 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
3 | orcom 401 | . 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓)) | |
4 | orcom 401 | . 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 303 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∨ wo 382 |
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 197 df-or 384 |
This theorem is referenced by: orbi1 742 orbi12d 746 eueq2 3413 uneq1 3793 r19.45zv 4101 rexprg 4267 rextpg 4269 swopolem 5073 ordsseleq 5790 ordtri3 5797 infltoreq 8449 cantnflem1 8624 axgroth2 9685 axgroth3 9691 lelttric 10182 ltxr 11987 xmulneg1 12137 fzpr 12434 elfzp12 12457 caubnd 14142 lcmval 15352 lcmass 15374 isprm6 15473 vdwlem10 15741 irredmul 18755 domneq0 19345 opsrval 19522 znfld 19957 logreclem 24545 perfectlem2 25000 legov3 25538 lnhl 25555 colperpex 25670 lmif 25722 islmib 25724 friendshipgt3 27385 h1datom 28569 xrlelttric 29645 tlt3 29793 esumpcvgval 30268 sibfof 30530 segcon2 32337 poimirlem25 33564 cnambfre 33588 pridl 33966 ismaxidl 33969 ispridlc 33999 pridlc 34000 dmnnzd 34004 4atlem3a 35201 pmapjoin 35456 lcfl3 37100 lcfl4N 37101 sbc3orgOLD 39059 fourierdlem80 40721 el1fzopredsuc 41660 perfectALTVlem2 41956 nnsum3primesle9 42007 lindslinindsimp2 42577 |
Copyright terms: Public domain | W3C validator |