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 132 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | 2 | orim2d 702 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒))) |
4 | 1 | biimprd 147 | . . 3 ⊢ (𝜑 → (𝜒 → 𝜓)) |
5 | 4 | orim2d 702 | . 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜒) → (𝜃 ∨ 𝜓))) |
6 | 3, 5 | impbid 120 | 1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 ∨ wo 629 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: orbi1d 705 orbi12d 707 dn1dc 867 xorbi2d 1271 eueq2dc 2714 rexprg 3422 rextpg 3424 swopolem 4042 sowlin 4057 elsucg 4141 elsuc2g 4142 ordsoexmid 4286 poleloe 4724 isosolem 5463 freceq2 5980 brdifun 6133 pitric 6419 elinp 6572 prloc 6589 ltexprlemloc 6705 ltsosr 6849 aptisr 6863 axpre-ltwlin 6957 gt0add 7564 apreap 7578 apreim 7594 elznn0 8260 elznn 8261 peano2z 8281 zindd 8356 elfzp1 8934 fzm1 8962 fzosplitsni 9091 cjap 9506 bj-nn0sucALT 10103 |
Copyright terms: Public domain | W3C validator |