![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orim2i | GIF version |
Description: Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
Ref | Expression |
---|---|
orim1i.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
orim2i | ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (𝜒 → 𝜒) | |
2 | orim1i.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | orim12i 759 | 1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 708 |
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 709 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: orbi2i 762 pm1.5 765 pm2.3 775 ordi 816 dcn 842 pm2.25dc 893 dcan 933 axi12 1514 dveeq2or 1816 equs5or 1830 sb4or 1833 sb4bor 1835 nfsb2or 1837 sbequilem 1838 sbequi 1839 sbal1yz 2001 dvelimor 2018 exmodc 2076 r19.44av 2636 exmidundif 4205 exmidundifim 4206 exmid1stab 4207 elsuci 4402 acexmidlemcase 5867 undifdcss 6919 updjudhf 7075 ctssdccl 7107 zindd 9367 fiubm 10801 fsumsplitsn 11411 fprodcllem 11607 fprodsplitsn 11634 subctctexmid 14610 |
Copyright terms: Public domain | W3C validator |