![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > jaod | Unicode version |
Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.) (Revised by NM, 4-Apr-2013.) |
Ref | Expression |
---|---|
jaod.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
jaod.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
jaod |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jaod.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | com12 27 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | jaod.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | com12 27 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | jaoi 635 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | com12 27 |
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: mpjaod 637 jaao 638 orel2 644 pm2.621 665 mtord 696 jaodan 709 pm2.63 712 pm2.74 719 dedlema 875 dedlemb 876 oplem1 881 opthpr 3534 trsucss 4126 ordsucim 4192 onsucelsucr 4199 0elnn 4283 xpsspw 4393 relop 4429 fununi 4910 poxp 5794 nntri1 6013 nnmordi 6025 nnaordex 6036 nnm00 6038 swoord2 6072 elni2 6298 prubl 6469 distrlem4prl 6560 distrlem4pru 6561 ltxrlt 6882 recexre 7362 remulext1 7383 mulext1 7396 un0addcl 7991 un0mulcl 7992 elnnz 8031 zleloe 8068 zindd 8132 uzsplit 8724 fzm1 8732 expcl2lemap 8921 expnegzap 8943 expaddzap 8953 expmulzap 8955 bj-nntrans 9411 bj-nnelirr 9413 bj-findis 9439 |
Copyright terms: Public domain | W3C validator |