![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orbi1d | GIF version |
Description: Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
orbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
orbi1d | ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orbid.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | orbi2d 745 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
3 | orcom 688 | . 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓)) | |
4 | orcom 688 | . 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 222 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∨ wo 670 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orbi1 747 orbi12d 748 xorbi1d 1327 eueq2dc 2810 uneq1 3170 r19.45mv 3403 rexprg 3522 rextpg 3524 swopolem 4165 sowlin 4180 onsucelsucexmidlem1 4381 onsucelsucexmid 4383 ordsoexmid 4415 isosolem 5657 acexmidlema 5697 acexmidlemb 5698 acexmidlem2 5703 acexmidlemv 5704 freceq1 6219 elinp 7183 prloc 7200 ltsosr 7460 axpre-ltwlin 7568 apreap 8215 apreim 8231 sup3exmid 8573 nn01to3 9259 ltxr 9403 fzpr 9698 elfzp12 9720 lcmval 11537 lcmass 11559 isprm6 11618 |
Copyright terms: Public domain | W3C validator |