![]() |
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 675 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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 629 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: orbi2i 678 pm1.5 681 pm2.3 691 ordi 728 dcn 745 pm2.25dc 791 dcan 841 axi12 1404 dveeq2or 1694 equs5or 1708 sb4or 1711 sb4bor 1713 nfsb2or 1715 sbequilem 1716 sbequi 1717 sbal1yz 1874 dvelimor 1891 exmodc 1947 r19.44av 2463 elsuci 4106 acexmidlemcase 5450 zindd 8132 |
Copyright terms: Public domain | W3C validator |