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 304 | . 2 |
5 | 1, 4 | jca 304 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: syl12anc 1225 euan 2069 imadiflem 5261 supelti 6958 ltexnqq 7340 enq0sym 7364 enq0tr 7366 addclpr 7469 mulclpr 7504 ltexprlemopl 7533 ltexprlemlol 7534 ltexprlemopu 7535 ltexprlemupu 7536 suplocexprlemloc 7653 lemul12a 8748 fzass4 9987 elfz1b 10015 4fvwrd4 10065 leexp1a 10500 sqrt0rlem 10931 reumodprminv 12162 uptx 12815 distspace 12876 xmetxpbl 13049 bj-charfundc 13525 |
Copyright terms: Public domain | W3C validator |