![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > anim1d | Unicode version |
Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
anim1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
anim1d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anim1d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | idd 21 |
. 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: pm3.45 597 exdistrfor 1800 mopick2 2109 ssrexf 3217 ssrexv 3220 ssdif 3270 ssrin 3360 reupick 3419 disjss1 3986 copsexg 4244 po3nr 4310 coss2 4783 fununi 5284 fiintim 6927 recexprlemlol 7624 recexprlemupu 7626 icoshft 9988 2ffzeq 10138 qbtwnxr 10255 ico0 10259 r19.2uz 10997 bezoutlemzz 11997 bezoutlemaz 11998 neiss 13543 uptx 13667 txcn 13668 bj-charfundcALT 14443 |
Copyright terms: Public domain | W3C validator |