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 748 | 1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 697 |
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 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orbi2i 751 pm1.5 754 pm2.3 764 ordi 805 dcn 827 pm2.25dc 878 dcan 918 axi12 1494 dveeq2or 1788 equs5or 1802 sb4or 1805 sb4bor 1807 nfsb2or 1809 sbequilem 1810 sbequi 1811 sbal1yz 1974 dvelimor 1991 exmodc 2047 r19.44av 2588 exmidundif 4124 exmidundifim 4125 elsuci 4320 acexmidlemcase 5762 undifdcss 6804 updjudhf 6957 ctssdccl 6989 zindd 9162 fsumsplitsn 11172 exmid1stab 13184 subctctexmid 13185 |
Copyright terms: Public domain | W3C validator |