![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE 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 519 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | jca 519 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem is referenced by: syl12anc 1182 euan 2315 sbthlem9 7188 nqerf 8767 lemul12a 9828 lediv12a 9863 fzass4 11050 4fvwrd4 11080 leexp1a 11397 mreexexlem2d 13829 islmodd 15915 istps2OLD 16945 neitr 17202 restnlly 17502 llyrest 17505 llyidm 17508 uptx 17614 alexsubALTlem2 18036 alexsubALTlem4 18038 ivthlem3 19307 grpoidinv 21753 pjnmopi 23608 cdj1i 23893 xrofsup 24083 dya2iocnrect 24588 sitgfval 24612 erdszelem7 24840 rellyscon 24895 relexpadd 25095 rtrclreclem.min 25104 ax5seg 25785 axcontlem4 25814 segconeq 25852 ifscgr 25886 btwnconn1lem13 25941 btwnconn1lem14 25942 outsideofeq 25972 ellines 25994 itg2gt0cn 26163 frinfm 26331 heiborlem3 26416 isfldidl 26572 mzpincl 26685 mzpindd 26697 diophin 26725 pellexlem3 26788 pellexlem5 26790 stoweidlem1 27621 stoweidlem3 27623 stoweidlem14 27634 stoweidlem17 27637 stoweidlem57 27677 reuan 27829 swrdccatin12c 28032 usg2spot2nb 28172 bnj969 29027 bnj1463 29134 4atlem12 30098 cdleme48fv 30985 cdlemg35 31199 mapd0 32152 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 178 df-an 361 |
Copyright terms: Public domain | W3C validator |