![]() |
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 120 | . . 3 ⊢ (𝜑 → 𝜓) |
3 | 2 | orim2i 762 | . 2 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
4 | 1 | biimpri 133 | . . 3 ⊢ (𝜓 → 𝜑) |
5 | 4 | orim2i 762 | . 2 ⊢ ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑)) |
6 | 3, 5 | impbii 126 | 1 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ∨ wo 709 |
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 710 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: orbi1i 764 orbi12i 765 orass 768 or4 772 or42 773 orordir 775 dcnnOLD 850 orbididc 955 3orcomb 989 excxor 1389 xordc 1403 nf4dc 1681 nf4r 1682 19.44 1693 dveeq2 1826 dvelimALT 2022 dvelimfv 2023 dvelimor 2030 dcne 2371 unass 3307 undi 3398 undif3ss 3411 symdifxor 3416 undif4 3500 iinuniss 3984 ordsucim 4514 suc11g 4571 qfto 5033 nntri3or 6512 reapcotr 8573 elnn0 9196 elxnn0 9259 elnn1uz2 9625 nn01to3 9635 elxr 9794 xaddcom 9879 xnegdi 9886 xpncan 9889 xleadd1a 9891 lcmdvds 12097 mulgcddvds 12112 cncongr2 12122 pythagtrip 12301 bj-peano4 15104 apdifflemr 15193 |
Copyright terms: Public domain | W3C validator |