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 318 | 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: pm3.45 529 exdistrfor 1681 mopick2 1983 ssrexv 3005 ssdif 3078 ssrin 3162 reupick 3221 disjss1 3751 copsexg 3981 po3nr 4047 coss2 4492 fununi 4967 recexprlemlol 6724 recexprlemupu 6726 icoshft 8858 2ffzeq 8998 r19.2uz 9591 |
Copyright terms: Public domain | W3C validator |