![]() |
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 119 | . . 3 ⊢ (𝜑 → 𝜓) |
3 | 2 | orim2i 719 | . 2 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
4 | 1 | biimpri 132 | . . 3 ⊢ (𝜓 → 𝜑) |
5 | 4 | orim2i 719 | . 2 ⊢ ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑)) |
6 | 3, 5 | impbii 125 | 1 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 670 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orbi1i 721 orbi12i 722 orass 725 or4 729 or42 730 orordir 732 testbitestn 867 orbididc 905 3orcomb 939 excxor 1324 xordc 1338 nf4dc 1616 nf4r 1617 19.44 1628 dveeq2 1754 dvelimALT 1946 dvelimfv 1947 dvelimor 1954 dcne 2278 unass 3180 undi 3271 undif3ss 3284 symdifxor 3289 undif4 3372 iinuniss 3841 ordsucim 4354 suc11g 4410 qfto 4864 nntri3or 6319 reapcotr 8226 elnn0 8831 elxnn0 8894 elnn1uz2 9251 nn01to3 9259 elxr 9404 xaddcom 9485 xnegdi 9492 xpncan 9495 xleadd1a 9497 lcmdvds 11553 mulgcddvds 11568 cncongr2 11578 bj-peano4 12738 |
Copyright terms: Public domain | W3C validator |