![]() |
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 302 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | jca 302 |
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-ia3 107 |
This theorem is referenced by: syl12anc 1197 euan 2031 imadiflem 5160 supelti 6841 ltexnqq 7164 enq0sym 7188 enq0tr 7190 addclpr 7293 mulclpr 7328 ltexprlemopl 7357 ltexprlemlol 7358 ltexprlemopu 7359 ltexprlemupu 7360 lemul12a 8530 fzass4 9735 elfz1b 9763 4fvwrd4 9810 leexp1a 10241 sqrt0rlem 10667 uptx 12285 distspace 12324 xmetxpbl 12497 |
Copyright terms: Public domain | W3C validator |