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 676 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wo 629 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: orbi2i 679 pm1.5 682 pm2.3 692 ordi 729 dcn 746 pm2.25dc 792 dcan 842 axi12 1407 dveeq2or 1697 equs5or 1711 sb4or 1714 sb4bor 1716 nfsb2or 1718 sbequilem 1719 sbequi 1720 sbal1yz 1877 dvelimor 1894 exmodc 1950 r19.44av 2469 elsuci 4140 acexmidlemcase 5507 zindd 8356 |
Copyright terms: Public domain | W3C validator |