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 293 | 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-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: anim1d 334 anim2d 335 anim12 342 im2anan9 588 anim12dan 590 3anim123d 1308 hband 1476 hbbid 1562 spsbim 1830 moim 2077 moimv 2079 2euswapdc 2104 rspcimedv 2827 soss 4286 trin2 4989 xp11m 5036 funss 5201 fun 5354 dff13 5730 f1eqcocnv 5753 isores3 5777 isosolem 5786 f1o2ndf1 6187 tposfn2 6225 tposf1o2 6229 nndifsnid 6466 nnaordex 6486 supmoti 6949 isotilem 6962 recexprlemss1l 7567 recexprlemss1u 7568 caucvgsrlemoffres 7732 suplocsrlem 7740 nnindnn 7825 eqord1 8372 lemul12b 8747 lt2msq 8772 lbreu 8831 cju 8847 nnind 8864 uz11 9479 xrre2 9748 ico0 10187 ioc0 10188 expcan 10618 gcdaddm 11902 bezoutlemaz 11921 bezoutlembz 11922 isprm3 12029 prmdiveq 12147 epttop 12637 cnptopresti 12785 cnptoprest 12786 txcnp 12818 addcncntoplem 13098 mulcncflem 13137 bj-stand 13469 exmidsbthrlem 13742 |
Copyright terms: Public domain | W3C validator |