![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > jca31 | Unicode version |
Description: Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.) |
Ref | Expression |
---|---|
jca31.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
jca31.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
jca31.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
jca31 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jca31.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | jca31.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | jca 306 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | jca31.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 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: 3jca 1177 syl21anbrc 1182 syl21anc 1237 f1oiso2 5827 exmidapne 7258 nnnq0lem1 7444 prmuloc 7564 suplocexprlemex 7720 prsrlem1 7740 apreap 8542 lemulge11 8821 elnnz 9261 supinfneg 9593 infsupneg 9594 leexp1a 10572 faclbnd6 10719 zfz1isolem1 10815 oddpwdclemdc 12167 ennnfonelemf1 12413 grpidinv2 12922 dvdsrzring 13424 cncnp2m 13662 bj-charfun 14479 |
Copyright terms: Public domain | W3C validator |