![]() |
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 142 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2 | orim2d 735 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒))) |
4 | 1 | biimprd 156 | . . 3 ⊢ (𝜑 → (𝜒 → 𝜓)) |
5 | 4 | orim2d 735 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜒) → (𝜃 ∨ 𝜓))) |
6 | 3, 5 | impbid 127 | 1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 ∨ wo 662 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: orbi1d 738 orbi12d 740 dn1dc 902 xorbi2d 1312 eueq2dc 2774 r19.44mv 3352 rexprg 3462 rextpg 3464 swopolem 4088 sowlin 4103 elsucg 4187 elsuc2g 4188 ordsoexmid 4333 poleloe 4774 isosolem 5515 freceq2 6063 brdifun 6221 pitric 6643 elinp 6796 prloc 6813 ltexprlemloc 6929 ltsosr 7073 aptisr 7087 axpre-ltwlin 7181 gt0add 7810 apreap 7824 apreim 7840 elznn0 8517 elznn 8518 peano2z 8538 zindd 8616 elfzp1 9235 fzm1 9263 fzosplitsni 9391 cjap 10012 dvdslelemd 10469 zeo5 10513 lcmval 10670 lcmneg 10681 lcmass 10692 isprm6 10751 bj-nn0sucALT 11058 |
Copyright terms: Public domain | W3C validator |