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 915 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
3 | orcom 869 | . 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓)) | |
4 | orcom 869 | . 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∨ wo 846 |
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 847 |
This theorem is referenced by: orbi1 917 orbi12d 918 eueq2 3667 uneq1 4115 r19.45zv 4459 rexprgf 4653 rextpg 4659 swopolem 5553 ordsseleq 6343 ordtri3 6350 infltoreq 9372 cantnflem1 9559 axgroth2 10695 axgroth3 10701 lelttric 11196 ltxr 12965 xmulneg1 13117 fzpr 13425 elfzp12 13449 caubnd 15178 lcmval 16403 lcmass 16425 isprm6 16525 vdwlem10 16797 irredmul 20062 domneq0 20691 znfld 20891 opsrval 21370 logreclem 26035 perfectlem2 26501 legov3 27339 lnhl 27356 colperpex 27474 lmif 27526 islmib 27528 friendshipgt3 29141 h1datom 30323 xrlelttric 31452 tlt3 31625 prmidl 32002 ismxidl 32021 esumpcvgval 32451 sibfof 32714 satfvsuc 33729 satfv1 33731 satfvsucsuc 33733 satf0suc 33744 sat1el2xp 33747 fmlasuc0 33752 fmlafvel 33753 satfv1fvfmla1 33791 frxp2 34180 xpord2pred 34181 xpord2ind 34183 frxp3 34186 xpord3pred 34187 segcon2 34586 wl-ifpimpr 35833 poimirlem25 35999 cnambfre 36022 pridl 36392 ismaxidl 36395 ispridlc 36425 pridlc 36426 dmnnzd 36430 disjecxrncnvep 36748 4atlem3a 37956 pmapjoin 38211 lcfl3 39853 lcfl4N 39854 sticksstones22 40472 sbcoreleleqVD 42906 fourierdlem80 44182 euoreqb 45096 el1fzopredsuc 45312 perfectALTVlem2 45669 nnsum3primesle9 45741 lindslinindsimp2 46299 |
Copyright terms: Public domain | W3C validator |