Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > orim2i | Unicode 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 749 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wo 698 |
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 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orbi2i 752 pm1.5 755 pm2.3 765 ordi 806 dcn 828 pm2.25dc 879 dcan 919 axi12 1495 dveeq2or 1789 equs5or 1803 sb4or 1806 sb4bor 1808 nfsb2or 1810 sbequilem 1811 sbequi 1812 sbal1yz 1977 dvelimor 1994 exmodc 2050 r19.44av 2593 exmidundif 4137 exmidundifim 4138 elsuci 4333 acexmidlemcase 5777 undifdcss 6819 updjudhf 6972 ctssdccl 7004 zindd 9193 fsumsplitsn 11211 exmid1stab 13368 subctctexmid 13369 |
Copyright terms: Public domain | W3C validator |