Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > anim2d | Unicode version |
Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
anim1d.1 |
Ref | Expression |
---|---|
anim2d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idd 21 | . 2 | |
2 | anim1d.1 | . 2 | |
3 | 1, 2 | anim12d 333 | 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: spsbim 1830 ssel 3131 sscon 3251 uniss 3804 trel3 4082 copsexg 4216 ssopab2 4247 coss1 4753 fununi 5250 imadif 5262 fss 5343 ssimaex 5541 opabbrex 5877 ssoprab2 5889 poxp 6191 pmss12g 6632 ss2ixp 6668 xpdom2 6788 qbtwnxr 10183 ioc0 10188 climshftlemg 11229 bezoutlembz 11922 tgcl 12611 neipsm 12701 ssnei2 12704 tgcnp 12756 cnpnei 12766 cnptopco 12769 mopni3 13031 limcresi 13182 cnlimcim 13187 |
Copyright terms: Public domain | W3C validator |