![]() |
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 12966 xmulneg1 13118 fzpr 13426 elfzp12 13450 caubnd 15179 lcmval 16404 lcmass 16426 isprm6 16526 vdwlem10 16798 irredmul 20067 domneq0 20696 znfld 20896 opsrval 21375 logreclem 26040 perfectlem2 26506 legov3 27345 lnhl 27362 colperpex 27480 lmif 27532 islmib 27534 friendshipgt3 29147 h1datom 30329 xrlelttric 31458 tlt3 31631 prmidl 32008 ismxidl 32027 esumpcvgval 32457 sibfof 32720 satfvsuc 33735 satfv1 33737 satfvsucsuc 33739 satf0suc 33750 sat1el2xp 33753 fmlasuc0 33758 fmlafvel 33759 satfv1fvfmla1 33797 frxp2 34183 xpord2pred 34184 xpord2ind 34186 frxp3 34189 xpord3pred 34190 segcon2 34621 wl-ifpimpr 35868 poimirlem25 36034 cnambfre 36057 pridl 36427 ismaxidl 36430 ispridlc 36460 pridlc 36461 dmnnzd 36465 disjecxrncnvep 36783 4atlem3a 37991 pmapjoin 38246 lcfl3 39888 lcfl4N 39889 sticksstones22 40507 sbcoreleleqVD 42942 fourierdlem80 44218 euoreqb 45132 el1fzopredsuc 45348 perfectALTVlem2 45705 nnsum3primesle9 45777 lindslinindsimp2 46335 |
Copyright terms: Public domain | W3C validator |