![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orbi2d | GIF version |
Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
orbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
orbi2d | ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orbid.1 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | biimpd 144 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2 | orim2d 788 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒))) |
4 | 1 | biimprd 158 | . . 3 ⊢ (𝜑 → (𝜒 → 𝜓)) |
5 | 4 | orim2d 788 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜒) → (𝜃 ∨ 𝜓))) |
6 | 3, 5 | impbid 129 | 1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∨ wo 708 |
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 709 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: orbi1d 791 orbi12d 793 dn1dc 960 xorbi2d 1380 eueq2dc 2910 r19.44mv 3517 rexprg 3643 rextpg 3645 exmidsssn 4199 exmidsssnc 4200 swopolem 4301 sowlin 4316 elsucg 4400 elsuc2g 4401 ordsoexmid 4557 poleloe 5023 isosolem 5818 freceq2 6387 brdifun 6555 pitric 7298 elinp 7451 prloc 7468 ltexprlemloc 7584 suplocexprlemloc 7698 ltsosr 7741 aptisr 7756 suplocsrlemb 7783 axpre-ltwlin 7860 axpre-suploclemres 7878 axpre-suploc 7879 gt0add 8507 apreap 8521 apreim 8537 elznn0 9244 elznn 9245 peano2z 9265 zindd 9347 elfzp1 10045 fzm1 10073 fzosplitsni 10208 cjap 10886 dvdslelemd 11819 zeo5 11863 lcmval 12033 lcmneg 12044 lcmass 12055 isprm6 12117 infpn2 12427 dedekindeulemloc 13730 dedekindeulemeu 13733 suplociccreex 13735 dedekindicclemloc 13739 dedekindicclemeu 13742 bj-charfunr 14184 bj-nn0sucALT 14352 |
Copyright terms: Public domain | W3C validator |