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 733 | 1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 682 |
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 683 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orbi2i 736 pm1.5 739 pm2.3 749 ordi 790 dcn 812 pm2.25dc 863 dcan 903 axi12 1479 dveeq2or 1772 equs5or 1786 sb4or 1789 sb4bor 1791 nfsb2or 1793 sbequilem 1794 sbequi 1795 sbal1yz 1954 dvelimor 1971 exmodc 2027 r19.44av 2567 exmidundif 4099 exmidundifim 4100 elsuci 4295 acexmidlemcase 5737 undifdcss 6779 updjudhf 6932 ctssdccl 6964 zindd 9137 fsumsplitsn 11147 exmid1stab 13122 subctctexmid 13123 |
Copyright terms: Public domain | W3C validator |