![]() |
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 791 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
3 | orcom 729 | . 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓)) | |
4 | orcom 729 | . 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 223 | 1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∨ wo 709 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: orbi1 793 orbi12d 794 xorbi1d 1392 eueq2dc 2925 uneq1 3297 r19.45mv 3531 rexprg 3659 rextpg 3661 swopolem 4323 sowlin 4338 onsucelsucexmidlem1 4545 onsucelsucexmid 4547 ordsoexmid 4579 isosolem 5845 acexmidlema 5886 acexmidlemb 5887 acexmidlem2 5892 acexmidlemv 5893 freceq1 6416 exmidaclem 7236 exmidac 7237 elinp 7502 prloc 7519 suplocexprlemloc 7749 ltsosr 7792 suplocsrlemb 7834 axpre-ltwlin 7911 axpre-suploclemres 7929 axpre-suploc 7930 apreap 8573 apreim 8589 sup3exmid 8943 nn01to3 9646 ltxr 9804 fzpr 10106 elfzp12 10128 lcmval 12094 lcmass 12116 isprm6 12178 lringuplu 13540 dedekindeulemloc 14549 dedekindeulemeu 14552 suplociccreex 14554 dedekindicclemloc 14558 dedekindicclemeu 14561 |
Copyright terms: Public domain | W3C validator |