![]() |
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 914 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
3 | orcom 868 | . 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓)) | |
4 | orcom 868 | . 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 313 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∨ wo 845 |
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 846 |
This theorem is referenced by: orbi1 916 orbi12d 917 eueq2 3671 uneq1 4121 r19.45zv 4465 rexprgf 4659 rextpg 4665 swopolem 5560 ordsseleq 6351 ordtri3 6358 frxp2 8081 xpord2pred 8082 xpord2indlem 8084 frxp3 8088 xpord3pred 8089 infltoreq 9447 cantnflem1 9634 axgroth2 10770 axgroth3 10776 lelttric 11271 ltxr 13045 xmulneg1 13198 fzpr 13506 elfzp12 13530 caubnd 15255 lcmval 16479 lcmass 16501 isprm6 16601 vdwlem10 16873 irredmul 20154 lringuplu 20224 domneq0 20804 znfld 21004 opsrval 21484 logreclem 26149 perfectlem2 26615 legov3 27603 lnhl 27620 colperpex 27738 lmif 27790 islmib 27792 friendshipgt3 29405 h1datom 30587 xrlelttric 31725 tlt3 31900 prmidl 32288 ismxidl 32307 esumpcvgval 32766 sibfof 33029 satfvsuc 34042 satfv1 34044 satfvsucsuc 34046 satf0suc 34057 sat1el2xp 34060 fmlasuc0 34065 fmlafvel 34066 satfv1fvfmla1 34104 segcon2 34766 wl-ifpimpr 36010 poimirlem25 36176 cnambfre 36199 pridl 36569 ismaxidl 36572 ispridlc 36602 pridlc 36603 dmnnzd 36607 disjecxrncnvep 36925 4atlem3a 38133 pmapjoin 38388 lcfl3 40030 lcfl4N 40031 sticksstones22 40649 ordsssucb 41728 sbcoreleleqVD 43263 fourierdlem80 44547 euoreqb 45461 el1fzopredsuc 45677 perfectALTVlem2 46034 nnsum3primesle9 46106 lindslinindsimp2 46664 |
Copyright terms: Public domain | W3C validator |