Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > anim12d | Unicode version |
Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.) |
Ref | Expression |
---|---|
anim12d.1 | |
anim12d.2 |
Ref | Expression |
---|---|
anim12d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anim12d.1 | . 2 | |
2 | anim12d.2 | . 2 | |
3 | idd 21 | . 2 | |
4 | 1, 2, 3 | syl2and 279 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: anim1d 319 anim2d 320 prth 326 im2anan9 530 anim12dan 532 3anim123d 1214 hband 1378 hbbid 1467 spsbim 1724 moim 1964 moimv 1966 2euswapdc 1991 rspcimedv 2658 soss 4051 trin2 4716 xp11m 4759 funss 4920 fun 5063 dff13 5407 f1eqcocnv 5431 isores3 5455 isosolem 5463 f1o2ndf1 5849 tposfn2 5881 tposf1o2 5885 nnaordex 6100 recexprlemss1l 6733 recexprlemss1u 6734 caucvgsrlemoffres 6884 nnindnn 6967 lemul12b 7827 lt2msq 7852 cju 7913 nnind 7930 uz11 8495 xrre2 8734 |
Copyright terms: Public domain | W3C validator |