![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orbi2i | GIF version |
Description: Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.) |
Ref | Expression |
---|---|
orbi2i.1 | ⊢ (φ ↔ ψ) |
Ref | Expression |
---|---|
orbi2i | ⊢ ((χ ∨ φ) ↔ (χ ∨ ψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orbi2i.1 | . . . 4 ⊢ (φ ↔ ψ) | |
2 | 1 | biimpi 113 | . . 3 ⊢ (φ → ψ) |
3 | 2 | orim2i 677 | . 2 ⊢ ((χ ∨ φ) → (χ ∨ ψ)) |
4 | 1 | biimpri 124 | . . 3 ⊢ (ψ → φ) |
5 | 4 | orim2i 677 | . 2 ⊢ ((χ ∨ ψ) → (χ ∨ φ)) |
6 | 3, 5 | impbii 117 | 1 ⊢ ((χ ∨ φ) ↔ (χ ∨ ψ)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ∨ wo 628 |
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 629 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: orbi1i 679 orbi12i 680 orass 683 or4 687 or42 688 orordir 690 testbitestn 822 orbididc 859 3orcomb 893 excxor 1268 xordc 1280 nf4dc 1557 nf4r 1558 19.44 1569 dveeq2 1693 dvelimALT 1883 dvelimfv 1884 dvelimor 1891 dcne 2211 unass 3094 undi 3179 undif3ss 3192 symdifxor 3197 undif4 3278 iinuniss 3728 ordsucim 4192 suc11g 4235 qfto 4657 nntri3or 6011 reapcotr 7382 elnn0 7959 elnn1uz2 8320 nn01to3 8328 elxr 8466 bj-peano4 9415 |
Copyright terms: Public domain | W3C validator |