![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > jca32 | Unicode version |
Description: Join three consequents. (Contributed by FL, 1-Aug-2009.) |
Ref | Expression |
---|---|
jca31.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
jca31.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
jca31.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
jca32 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jca31.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | jca31.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | jca31.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | jca 306 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | jca 306 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: syl12anc 1247 euan 2094 imadiflem 5314 supelti 7030 ltexnqq 7436 enq0sym 7460 enq0tr 7462 addclpr 7565 mulclpr 7600 ltexprlemopl 7629 ltexprlemlol 7630 ltexprlemopu 7631 ltexprlemupu 7632 suplocexprlemloc 7749 lemul12a 8848 elfzd 10045 fzass4 10091 elfz1b 10119 4fvwrd4 10169 leexp1a 10605 sqrt0rlem 11043 reumodprminv 12284 islmodd 13606 uptx 14226 distspace 14287 xmetxpbl 14460 bj-charfundc 15013 |
Copyright terms: Public domain | W3C validator |