Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > anim2i | Unicode version |
Description: Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
anim1i.1 |
Ref | Expression |
---|---|
anim2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 | |
2 | anim1i.1 | . 2 | |
3 | 1, 2 | anim12i 336 | 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 is referenced by: sylanl2 400 sylanr2 402 andi 792 pm4.55dc 907 xoranor 1340 19.41h 1648 sbimi 1722 equs5e 1751 exdistrfor 1756 equs45f 1758 sbidm 1807 eu3h 2022 eupickb 2058 2exeu 2069 darii 2077 festino 2083 baroco 2084 r19.27v 2536 r19.27av 2544 rspc2ev 2778 reu3 2847 difdif 3171 ssddif 3280 inssdif 3282 difin 3283 difindiss 3300 indifdir 3302 difrab 3320 iundif2ss 3848 trssord 4272 ordsuc 4448 find 4483 imainss 4924 dffun5r 5105 fof 5315 f1ocnv 5348 fv3 5412 relelfvdm 5421 funimass4 5440 fvelimab 5445 funconstss 5506 dff2 5532 dffo5 5537 dff1o6 5645 oprabid 5771 ssoprab2i 5828 releldm2 6051 ixpf 6582 recexgt0sr 7549 map2psrprg 7581 lediv2a 8617 lbreu 8667 elfzp12 9834 focdmex 10488 fihashf1rn 10490 cau3lem 10841 fsumcl2lem 11122 dvdsnegb 11422 dvds2add 11439 dvds2sub 11440 ndvdssub 11539 gcd2n0cl 11570 divgcdcoprmex 11695 cncongr1 11696 ctinfom 11852 istopfin 12078 toponcom 12105 cnptoprest 12319 |
Copyright terms: Public domain | W3C validator |