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 304 | . 2 |
4 | jca31.3 | . 2 | |
5 | 3, 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: 3jca 1146 syl21anc 1200 f1oiso2 5696 nnnq0lem1 7222 prmuloc 7342 suplocexprlemex 7498 prsrlem1 7518 apreap 8317 lemulge11 8592 elnnz 9032 supinfneg 9358 infsupneg 9359 leexp1a 10316 faclbnd6 10458 zfz1isolem1 10551 oddpwdclemdc 11778 ennnfonelemf1 11858 cncnp2m 12327 |
Copyright terms: Public domain | W3C validator |