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 1166 syl21anbrc 1171 syl21anc 1226 f1oiso2 5789 nnnq0lem1 7378 prmuloc 7498 suplocexprlemex 7654 prsrlem1 7674 apreap 8476 lemulge11 8752 elnnz 9192 supinfneg 9524 infsupneg 9525 leexp1a 10500 faclbnd6 10646 zfz1isolem1 10739 oddpwdclemdc 12084 ennnfonelemf1 12294 cncnp2m 12778 bj-charfun 13530 |
Copyright terms: Public domain | W3C validator |