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 785 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
3 | orcom 723 | . 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓)) | |
4 | orcom 723 | . 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 222 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∨ wo 703 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orbi1 787 orbi12d 788 xorbi1d 1376 eueq2dc 2903 uneq1 3274 r19.45mv 3507 rexprg 3633 rextpg 3635 swopolem 4288 sowlin 4303 onsucelsucexmidlem1 4510 onsucelsucexmid 4512 ordsoexmid 4544 isosolem 5800 acexmidlema 5841 acexmidlemb 5842 acexmidlem2 5847 acexmidlemv 5848 freceq1 6368 exmidaclem 7172 exmidac 7173 elinp 7423 prloc 7440 suplocexprlemloc 7670 ltsosr 7713 suplocsrlemb 7755 axpre-ltwlin 7832 axpre-suploclemres 7850 axpre-suploc 7851 apreap 8493 apreim 8509 sup3exmid 8860 nn01to3 9563 ltxr 9719 fzpr 10020 elfzp12 10042 lcmval 12004 lcmass 12026 isprm6 12088 dedekindeulemloc 13312 dedekindeulemeu 13315 suplociccreex 13317 dedekindicclemloc 13321 dedekindicclemeu 13324 |
Copyright terms: Public domain | W3C validator |