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 756 | . 2 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
4 | 1 | biimpri 132 | . . 3 ⊢ (𝜓 → 𝜑) |
5 | 4 | orim2i 756 | . 2 ⊢ ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑)) |
6 | 3, 5 | impbii 125 | 1 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ∨ wo 703 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orbi1i 758 orbi12i 759 orass 762 or4 766 or42 767 orordir 769 dcnnOLD 844 orbididc 948 3orcomb 982 excxor 1373 xordc 1387 nf4dc 1663 nf4r 1664 19.44 1675 dveeq2 1808 dvelimALT 2003 dvelimfv 2004 dvelimor 2011 dcne 2351 unass 3284 undi 3375 undif3ss 3388 symdifxor 3393 undif4 3476 iinuniss 3953 ordsucim 4482 suc11g 4539 qfto 4998 nntri3or 6469 reapcotr 8504 elnn0 9124 elxnn0 9187 elnn1uz2 9553 nn01to3 9563 elxr 9720 xaddcom 9805 xnegdi 9812 xpncan 9815 xleadd1a 9817 lcmdvds 12020 mulgcddvds 12035 cncongr2 12045 pythagtrip 12224 bj-peano4 13912 apdifflemr 14001 |
Copyright terms: Public domain | W3C validator |