![]() |
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 335 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: spsbim 1843 ssel 3149 sscon 3269 uniss 3828 trel3 4106 copsexg 4240 ssopab2 4271 coss1 4777 fununi 5279 imadif 5291 fss 5372 ssimaex 5572 opabbrex 5912 ssoprab2 5924 poxp 6226 pmss12g 6668 ss2ixp 6704 xpdom2 6824 qbtwnxr 10231 ioc0 10236 climshftlemg 11281 bezoutlembz 11975 tgcl 13197 neipsm 13287 ssnei2 13290 tgcnp 13342 cnpnei 13352 cnptopco 13355 mopni3 13617 limcresi 13768 cnlimcim 13773 |
Copyright terms: Public domain | W3C validator |